EPR-Based Bounded Model Checking at Word Level?

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 un-rolled transition systems and facilitates reasoning at a higher level of abstrac-tion. We show that the proposed approach can be scaled to industrial hardware model checking problems involving memories and bit-vectors. Another contribu-tion of this work is in generating challenging benchmarks for first-order theorem provers based on the proposed encoding of real-life hardware verification prob-lems into EPR. We report experimental results for these problems for several provers known to be strong in EPR problem solving. A number of these bench-marks have already been released to the TPTP library.