Sciweavers

CADE
2012
Springer

EPR-Based Bounded Model Checking at Word Level

12 years 17 days ago
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.
Moshe Emmer, Zurab Khasidashvili, Konstantin Korov
Added 29 Sep 2012
Updated 29 Sep 2012
Type Journal
Year 2012
Where CADE
Authors Moshe Emmer, Zurab Khasidashvili, Konstantin Korovin, Christoph Sticksel, Andrei Voronkov
Comments (0)