@inproceedings{Emmer2012EPR-based,
    abstract = {We propose a word level, bounded model checking (BMC) algorithm based on translation into the effectively propositional  fragment (EPR) of first-order logic. This approach to BMC allows for succinct representation of unrolled transition systems and facilitates reasoning at a higher level of abstraction. We show that the proposed approach can be scaled to industrial hardware model checking problems involving memories and bit-vectors. Another contribution of this work is in generating challenging benchmarks for first-order theorem provers based on the proposed encoding of real-life hardware verification problems into EPR. We report experimental results for these problems for several provers known to be strong in EPR problem solving. A number of these benchmarks have already been released to the TPTP library.},
    address = {Berlin / Heidelberg},
    author = {Moshe Emmer and Zurab Khasidashvili and Konstantin Korovin and Christoph Sticksel and Andrei Voronkov},
    booktitle = {6th International Joint Conference on Automated Reasoning, IJCAR 2012},
    journal = {Automated Reasoning},
    location = {Manchester, UK},
    publisher = {Springer},
    series = {Lecture Notes in Computer Science},
    title = {EPR-Based Bounded Model Checking at Word Level},
    year = {2012}
}