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.
This work is partially supported by EPSRC, the Royal Society and a grant from Intel.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abu-Haimed, H., Dill, D.L., Berezin, S.: A refinement method for validity checking of quantified first-order formulas in hardware verification. In: FMCAD 2006 (2006)
Alberti, F., Armando, A., Ranise, S.: ASASP: Automated Symbolic Analysis of Security Policies. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol. 6803, pp. 26–33. Springer, Heidelberg (2011)
Baumgartner, P., Fuchs, A., Tinelli, C.: Implementing the Model Evolution Calculus. Inter. J. on Artificial Intelligence Tools 15(1), 21–52 (2006)
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)
Bradley, A.R.: SAT-Based Model Checking without Unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70–87. Springer, Heidelberg (2011)
Bradley, A.R., Manna, Z., Sipma, H.B.: What’s Decidable About Arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427–442. Springer, Heidelberg (2005)
Brummayer, R., Biere, A.: Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 174–177. Springer, Heidelberg (2009)
Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 78–92. Springer, Heidelberg (2002)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (1999)
Claessen, K., Sörensson, N.: New techniques that improve MACE-style model finding. In: Workshop on Model Computation, MODEL (2003)
Eén, N., Sörensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Eén, N., Sörensson, N.: Temporal induction by incremental SAT solving. ENTCS 89(4) (2003)
Emmer, M., Khasidashvili, Z., Korovin, K., Voronkov, A.: Encoding Industrial Hardware Verification Problems into Effectively Propositional Logic. In: FMCAD 2010 (2010)
Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Decision procedures for extensions of the theory of arrays. Annals of Mathematics and Artificial Intelligence, AMAI (2006)
Hoder, K., Khasidashvili, Z., Korovin, K., Voronkov, A.: Preprocessing techniques for first-order clausification (in preparation)
Huang, S.-Y., Cheng, K.-T.: Formal Equivalence Checking and Design Debugging. Kluwer (1998)
Khasidashvili, Z., Kinanah, M., Voronkov, A.: Verifying Equivalence of Memories Using a First Order Logic Theorem Prover. In: FMCAD 2009 (2009)
Khasidashvili, Z., Nadel, A.: Implicative simultaneous satisfiability and applications. In: HVC 2011 (2011)
Korovin, K.: iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 292–298. Springer, Heidelberg (2008)
Kovács, L., Voronkov, A.: Finding Loop Invariants for Programs over Arrays Using a Theorem Prover. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol. 5503, pp. 470–485. Springer, Heidelberg (2009)
Kroening, D., Strichman, O.: Decision Procedures. EATCS. Springer (2008)
Mishchenko, A., Chatterjee, S., Brayton, R., Een, N.: Improvements to combinational equivalence checking. In: ICCAD (2006)
Navarro-Pérez, J.A., Voronkov, A.: Encodings of Bounded LTL Model Checking in Effectively Propositional Logic. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 346–361. Springer, Heidelberg (2007)
Manolios, P., Srinivasan, S.K., Vroon, D.: Automatic memory reductions for RTL model verification. In: ICCAD (2006)
Piskac, R., de Moura, L., Bjørner, N.: Deciding Effectively Propositional Logic Using DPLL and Substitution Sets. J. Autom. Reasoning (2010)
Robinson, A., Voronkov, A. (eds.): Handbook of Automated Reasoning. Elsevier and MIT Press (2001)
Sutcliffe, G.: The 5th IJCAR automated theorem proving system competition CASC-J5. AI Communications 24(1), 75–89 (2011)
Velev, M.N., Bryant, R.E.: Verification of Pipelined Microprocessors by Comparing Memory Execution Sequences in Symbolic Simulation. In: Shyamasundar, R.K. (ed.) ASIAN 1997. LNCS, vol. 1345, pp. 18–31. Springer, Heidelberg (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Emmer, M., Khasidashvili, Z., Korovin, K., Sticksel, C., Voronkov, A. (2012). EPR-Based Bounded Model Checking at Word Level. In: Gramlich, B., Miller, D., Sattler, U. (eds) Automated Reasoning. IJCAR 2012. Lecture Notes in Computer Science(), vol 7364. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31365-3_18
Download citation
DOI: https://doi.org/10.1007/978-3-642-31365-3_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-31364-6
Online ISBN: 978-3-642-31365-3
eBook Packages: Computer ScienceComputer Science (R0)