×

zbMATH — the first resource for mathematics

Infinite-state invariant checking with IC3 and predicate abstraction. (English) Zbl 1368.68245
Summary: We address the problem of verifying invariant properties on infinite-state systems. We present a novel approach, IC3ia, for generalizing the IC3 invariant checking algorithm from finite-state to infinite-state transition systems, expressed over some background theories. The procedure is based on a tight integration of IC3 with Implicit Abstraction, a form of predicate abstraction that expresses abstract paths without computing explicitly the abstract system. In this scenario, IC3 operates only at the Boolean level of the abstract state space, discovering inductive clauses over the abstraction predicates. Theory reasoning is confined within the underlying SMT solver, and applied transparently when performing satisfiability checks. When the current abstraction allows for a spurious counterexample, it is refined by discovering and adding a sufficient set of new predicates. Importantly, this can be done in a completely incremental manner, without discarding the clauses found in the previous search. The proposed approach has two key advantages. First, unlike previous SMT generalizations of IC3, it allows to handle a wide range of background theories without relying on ad-hoc extensions, such as quantifier elimination or theory-specific clause generalization procedures, which might not always be available and are often highly inefficient. Second, compared to a direct exploration of the concrete transition system, the use of abstraction gives a significant performance improvement, as our experiments demonstrate.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Ball T, Majumdar R, Millstein TD, Rajamani SK (2001) Automatic predicate abstraction of C programs. In: PLDI, pp. 203-213
[2] Ball T, Podelski A, Rajamani SK (2002) Relative completeness of abstraction refinement for software model checking. In: Katoen JP, Stevens P (eds) TACS, LNCS, vol 2280. Springer, pp 158-172 · Zbl 1043.68523
[3] Ball, T; Podelski, A; Rajamani, SK, Boolean and Cartesian abstraction for model checking C programs, STTT, 5, 49-58, (2003) · Zbl 0978.68540
[4] Barrett CW, Sebastiani R, Seshia SA, Tinelli C (2009) Satisfiability modulo theories. In Handbook of satisfiability, vol 185. IOS Press, pp 825-885
[5] Baumgartner J, Ivrii A, Matsliah A, Mony H (2012) IC3-guided abstraction. In: Formal methods in computer-aided design (FMCAD 2012). Cambridge, UK, pp 182-185, 22-25 October 2012
[6] Beyer D (2013) Second competition on software verification—(Summary of SV-COMP 2013). In: TACAS, LNCS, vol 7795. Springer, pp 594-609
[7] Biere, A; Artho, C; Schuppan, V, Liveness checking as safety checking, Electr Notes Theor Comput Sci, 66, 160-177, (2002)
[8] Birgmeier J, Bradley AR, Weissenbacher G (2014) Counterexample to induction-guided abstraction-refinement (CTIGAR). In CAV, pp 831-848
[9] Bjørner N, Gurfinkel A (2015) Property directed polyhedral abstraction. In VMCAI, pp 263-281 · Zbl 1432.68257
[10] Bradley A. IC3ref. https://github.com/arbrad/IC3ref · Zbl 1325.68145
[11] Bradley A, Somenzi F, Hassan Z, Zhang Y (2011) An incremental approach to model checking progress properties. In: FMCAD · Zbl 1325.68145
[12] Bradley AR (2011) SAT-based model checking without unrolling. In: VMCAI, LNCS, vol 6538. Springer, pp 70-87 · Zbl 1317.68109
[13] Bradley AR, Manna Z (2007) Checking safety by inductive generalization of counterexamples to induction. In: FMCAD. IEEE Computer Society, pp 173-180
[14] Cavada R, Cimatti A, Dorigatti M, Griggio A, Mariotti A, Micheli A, Mover S, Roveri M, Tonetta S (2014) The nuXmv symbolic model checker. In CAV, LNCS, vol 8559, pp 334-342
[15] Cavada R, Cimatti A, Franzén A, Kalyanasundaram K, Roveri M, Shyamasundar RK (2007) Computing predicate abstractions by integrating BDDs and SMT solvers. In: FMCAD. IEEE Computer Society, pp 69-76
[16] Chokler H, Ivrii A, Matsliah A, Moran S, Nevo Z (2011) Incremental formal verification of hardware. In: FMCAD
[17] Cimatti A, Franzén A, Griggio A, Kalyanasundaram K, Roveri M (2010) Tighter integration of BDDs and SMT for predicate abstraction. In: DATE. IEEE, pp 1707-1712
[18] Cimatti A, Griggio A (2012) Software model checking via IC3. In: CAV, pp 277-293
[19] Cimatti A, Griggio A, Mover S, Tonetta S (2014) IC3 modulo theories via implicit predicate abstraction. In: TACAS, pp 46-61 · Zbl 1368.68245
[20] Cimatti A, Griggio A, Schaafsma B, Sebastiani R (2013) The MathSAT5 SMT solver. In: TACAS, LNCS, vol 7795. Springer · Zbl 1381.68153
[21] Cimatti, A; Griggio, A; Sebastiani, R, Efficient generation of Craig interpolants in satisfiability modulo theories, ACM Trans Comput Log, 12, 7, (2010) · Zbl 1351.68247
[22] Claessen K, Sörensson N (2012) A liveness checking algorithm that counts. In: FMCAD. IEEE, pp 52-59
[23] Clarke, EM; Grumberg, O; Jha, S; Lu, Y; Veith, H, Counterexample-guided abstraction refinement for symbolic model checking, J ACM, 50, 752-794, (2003) · Zbl 1325.68145
[24] Clarke, EM; Grumberg, O; Long, DE, Model checking and abstraction, ACM Trans Program Lang Syst, 16, 1512-1542, (1994)
[25] Een N, Mishchenko A, Brayton R (2011) Efficient implementation of property-directed reachability. In: FMCAD
[26] Graf S, Saïdi H (1997) Construction of abstract state graphs with PVS. In: CAV, pp 72-83
[27] Griggio A, Roveri M (2016) Comparing different variants of the IC3 algorithm for hardware model checking. IEEE Trans CAD Integr Circuits Syst 35(6):1026-1039
[28] Gupta A, Rybalchenko A (2009) InvGen: An efficient invariant generator. In: CAV, LNCS, vol 5643. Springer, pp 634-640
[29] Gupta A, Strichman O (2005) Abstraction refinement for bounded model checking. In: CAV, pp 112-124 · Zbl 1081.68620
[30] Gurfinkel A, Ivrii A (2015) Pushing to the top. In: Formal methods in computer-aided design (FMCAD 2015) Austin, Texas, USA, pp 65-72, 27-30 September 2015
[31] Hagen G, Tinelli C (2008) Scaling up the formal verification of lustre programs with SMT-based techniques. In: FMCAD. IEEE, pp 1-9
[32] Hassan Z, Bradley AR, Somenzi F (2013) Better generalization in IC3. In: FMCAD. IEEE, pp 157-164
[33] Henzinger TA, Jhala R, Majumdar R, McMillan KL (2004) Abstractions from proofs. In: POPL, pp 232-244 · Zbl 1325.68147
[34] Henzinger TA, Jhala R, Majumdar R, Sutre G (2002) Lazy abstraction. In: POPL, pp 58-70 · Zbl 1323.68374
[35] Hoder K, Bjørner N (2012) Generalized property directed reachability. In: SAT, pp 157-171 · Zbl 1273.68229
[36] Isenberg T, Wehrheim H (2014) Timed automata verification via IC3 with zones. In: ICFEM, pp 203-218
[37] Itzhaky S, Bjørner N, Reps TW, Sagiv M, Thakur AV (2014) Property-directed shape analysis. In: CAV, pp 35-51
[38] Jain H, Kroening D, Sharygina N, Clarke EM (2005) Word level predicate abstraction and refinement for verifying RTL verilog. In: DAC, pp 445-450
[39] Kahsai T, Tinelli C (2011) PKind: A parallel k-induction based model checker. In: PDMC, EPTCS, vol 72, pp 55-62 · Zbl 1351.68247
[40] Karbyshev A, Bjørner N, Itzhaky S, Rinetzky N, Shoham S (2015) Property-directed inference of universal invariants or proving their absence. In: CAV, pp 583-602 · Zbl 1381.68169
[41] Kindermann R, Junttila TA, Niemelä I (2012) SMT-based induction methods for timed systems. In: FORMATS, LNCS, vol 7595. Springer, pp 171-187 · Zbl 1374.68293
[42] Kurshan RP (1994) Computer aided verification of coordinating processes. Princeton University Press, Princeton · Zbl 0822.68116
[43] Lahiri SK, Nieuwenhuis R, Oliveras A (2006) SMT techniques for fast predicate abstraction. In: CAV, pp 424-437
[44] Lange T, Neuhäußer MR, Noll T (2015) IC3 software model checking on control flow automata. In: Formal methods in computer-aided design (FMCAD 2015) Austin, Texas, USA, pp 97-104, 27-30 September 2015
[45] McMillan KL (2006) Lazy Abstraction with Interpolants. In: CAV, LNCS, vol 4144. Springer, pp 123-136 · Zbl 1188.68196
[46] Sorensson N, Claessen K. Tip. https://github.com/niklasso/tip
[47] Tonetta S (2009) Abstract model checking without computing the abstraction. In: FM, pp 89-105
[48] Vizel Y, Grumberg O, Shoham S (2012) Lazy abstraction and SAT-based reachability in hardware model checking. In: FMCAD. IEEE, pp 173-181
[49] Vizel Y, Gurfinkel A (2014) Interpolating property directed reachability. In: CAV, pp 260-276
[50] Vizel Y, Weissenbacher G, Malik S (2015) Boolean satisfiability solvers and their applications in model checking. Proc IEEE 103(11):2021-2035
[51] Welp T, Kuehlmann A (2013) QF_BV model checking with property directed reachability. In: DATE, pp 791-796
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.