zbMATH — the first resource for mathematics

EPR-based bounded model checking at word level. (English) Zbl 1358.68190
Gramlich, Bernhard (ed.) et al., Automated reasoning. 6th international joint conference, IJCAR 2012, Manchester, UK, June 26–29, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-31364-6/pbk). Lecture Notes in Computer Science 7364. Lecture Notes in Artificial Intelligence, 210-224 (2012).
Summary: 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.
For the entire collection see [Zbl 1245.68010].

68Q60 Specification and verification (program logics, model checking, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI