×

zbMATH — the first resource for mathematics

SAT-based model checking without unrolling. (English) Zbl 1317.68109
Jhala, Ranjit (ed.) et al., Verification, model checking, and abstract interpretation. 12th international conference, VMCAI 2011, Austin, TX, USA, January 23–25, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-18274-7/pbk). Lecture Notes in Computer Science 6538, 70-87 (2011).
Summary: A new form of SAT-based symbolic model checking is described. Instead of unrolling the transition relation, it incrementally generates clauses that are inductive relative to (and augment) stepwise approximate reachability information. In this way, the algorithm gradually refines the property, eventually producing either an inductive strengthening of the property or a counterexample trace. Our experimental studies show that induction is a powerful tool for generalizing the unreachability of given error states: it can refine away many states at once, and it is effective at focusing the proof search on aspects of the transition system relevant to the property. Furthermore, the incremental structure of the algorithm lends itself to a parallel implementation.
For the entire collection see [Zbl 1206.68013].

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
Software:
MiniSat; Chaff
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Awedh, M., Somenzi, F.: Automatic invariant strengthening to prove properties in bounded model checking. In: DAC, pp. 1073–1076. ACM Press, New York (2006)
[2] Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)
[3] Biere, A., Claessen, K.: Hardware model checking competition. In: Hardware Verification Workshop (2010)
[4] Bradley, A.R.: Safety Analysis of Systems. PhD thesis, Stanford University (May 2007)
[5] Bradley, A.R.: k-step relative inductive generalization. Tech. Rep., CU Boulder (March 2010), http://arxiv.org/abs/1003.3649
[6] Bradley, A.R., Manna, Z.: Checking safety by inductive generalization of counterexamples to induction. In: FMCAD (2007)
[7] Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 10^20 states and beyond. Inf. Comput. 98(2), 142–170 (1992) · Zbl 0753.68066
[8] Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5) (2003) · Zbl 1325.68145
[9] Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)
[10] Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238–252. ACM Press, New York (1977)
[11] Eén, N.: Cut sweeping. Tech. rep., Cadence (2007)
[12] Eén, N., Biere, A.: Effective preprocessing in SAT through variable and clause elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61–75. Springer, Heidelberg (2005) · Zbl 1128.68463
[13] Eén, N., Mishchenko, A., Sörensson, N.: Applying logic synthesis for speeding up SAT. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 272–286. Springer, Heidelberg (2007) · Zbl 1214.68351
[14] 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) · Zbl 1204.68191
[15] Eén, N., Sörensson, N.: Temporal induction by incremental SAT solving. In: BMC (2003) · Zbl 1271.68215
[16] Floyd, R.W.: Assigning meanings to programs. In: Symposia in Applied Mathematics, vol. 19, pp. 19–32. American Mathematical Society, Providence (1967) · Zbl 0189.50204
[17] Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)
[18] Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12(10), 576–580 (1969) · Zbl 0179.23105
[19] Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995) · Zbl 1288.68169
[20] McMillan, K.L.: Applying SAT methods in unbounded symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 250–264. Springer, Heidelberg (2002) · Zbl 1010.68509
[21] McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003) · Zbl 1278.68184
[22] Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: DAC (2001)
[23] de Moura, L., Rueß, H., Sorea, M.: Bounded model checking and induction: From refutation to verification. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 14–26. Springer, Heidelberg (2003) · Zbl 1278.68199
[24] Sheeran, M., Singh, S., Stålmarck, G.: Checking safety properties using induction and a SAT-solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 108–125. Springer, Heidelberg (2000)
[25] Vimjam, V.C., Hsiao, M.S.: Fast illegal state identification for improving SAT-based induction. In: DAC, pp. 241–246. ACM Press, New York (2006)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.