EPR-Based Bounded Model Checking at Word Level

We propose a word level, bounded model checking (BMC) algorithm based on translation into the effectively propositional fragment (EPR) of firstorder 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.

• Type: Journal
• Year: 2012
• Where: CADE
• Authors: Moshe Emmer, Zurab Khasidashvili, Konstantin Korovin, Christoph Sticksel, Andrei Voronkov
• Keywords: CADE 2012, Logical Reasoning, Propositional Fragment, Succinct Representation, Tptp Library