×

An extension of lazy abstraction with interpolation for programs with arrays. (English) Zbl 1317.68107

Summary: Lazy abstraction with interpolation-based refinement has been shown to be a powerful technique for verifying imperative programs. In presence of arrays, however, the method suffers from an intrinsic limitation, due to the fact that invariants needed for verification usually contain universally quantified variables, which are not present in program specifications. In this work we present an extension of the interpolation-based lazy abstraction framework in which arrays of unknown length can be handled in a natural manner. In particular, we exploit the Model Checking Modulo Theories framework to derive a backward reachability version of lazy abstraction that supports reasoning about arrays. The new approach has been implemented in a tool, called safari, which has been validated on a wide range of benchmarks. We show by means of experiments that our approach can synthesize and prove universally quantified properties over arrays in a completely automatic fashion.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
PDF BibTeX XML Cite
Full Text: DOI Link

References:

[1] Abdulla, PA; Jonsson, B, Verifying programs with unreliable channels, Inf Comput, 127, 91-101, (1996) · Zbl 0856.68096
[2] Aho AV, Lam MS, Sethi R, Ullman JD (2007) Compilers: principles, techniques, and tools, 2nd edn. Pearson-Addison Wesley.
[3] Albarghouthi, A; Gurfinkel, A; Chechik, M; Miné, A (ed.); Schmidt, D (ed.), Craig interpretation, 300-316, (2012), Lecture Notes in Computer Science
[4] Alberti F, Bruttomesso R, Ghilardi S, Ranise S, Sharygina N (2012) Lazy abstraction with interpolants for arrays. In: Bjørner N, Voronkov A (eds) LPAR, Lecture Notes in Computer Science, vol 7180, pp 46-61. Springer. · Zbl 1352.68141
[5] Alberti F, Bruttomesso R, Ghilardi S, Ranise S, Sharygina N (2012) SAFARI: SMT-based abstraction for arrays with interpolants. In: Madhusudan P, Seshia SA (eds) CAV., Lecture Notes in Computer Science, vol 7358, Springer, Berlin, pp 679-685 · Zbl 1352.68141
[6] Alberti F, Ghilardi S, Pagani E, Ranise S, Rossi GP (2010). Automated support for the design and validation of fault tolerant parameterized systems: a case study. ECEASST, p 35. · Zbl 1335.68138
[7] Alberti, F; Ghilardi, S; Pagani, E; Ranise, S; Rossi, GP, Universal guards, relativization of quantifiers, and failure models in model checking modulo theories, JSAT, 8, 29-61, (2012) · Zbl 1331.68141
[8] Armando A, Benerecetti M, Carotenuto D, Mantovani J, Spica P (2007) The Eureka tool for software model checking. In Stirewalt REK, Egyed A, Fischer B (eds), ASE. ACM, pp 541-542.
[9] Armando A, Benerecetti M, Mantovani J (2007). Abstraction refinement of linear programs with arrays. In: Grumberg O, Huth M (eds) TACAS, Lecture Notes in Computer Science, vol 4424. Springer, pp 373-388. · Zbl 1186.68275
[10] Franz, Baader; Silvio, Ghilardi, No article title, Connecting many-sorted theories. J Symb Logic, 72, 535-583, (2007) · Zbl 1136.03012
[11] Ball T, Rajamani SK (2002) The SLAM project: debugging system software via static analysis. In: Launchbury and Mitchell (eds) Conference record of POPL 2002: The 29th SIGPLAN-SIGACT symposium on principles of programming languages, Portland, OR, USA, January 16-18, 2002. ACM, pp 1-3. · Zbl 1184.68461
[12] Beyer D (2013) Second competition on Software Verification-(Summary of SV-COMP 2013). In Piterman N, Smolka SA (eds) Proceedings of the 19th international conference on tools and algorithms for the construction and analysis of systems, TACAS 2013, held as part of the European joint conferences on theory and practice of software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Lecture Notes in Computer Science, vol 7795. Springer, pp 594-609
[13] Beyer D, Henzinger TA, Jhala R, Majumdar R (2007) The software model checker blast. STTT 9(5-6):505-525 · Zbl 0944.68139
[14] Beyer D, Henzinger TA, Jhala R, Majumdar R, Rybalchenko A (2007) Invariant synthesis for combined theories. In Cook B, Podelski A (eds) VMCAI, Lecture Notes in Computer Science, vol 4349. Springer, pp 378-394. · Zbl 1132.68333
[15] Beyer D, Erkan Keremoglu M (2011) CPAchecker: a tool for configurable software verification. In: Gopalakrishnan G, Qadeer S (eds) Proceedings of the 23rd international conference on computer aided verification, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Lecture Notes in Computer Science, vol 6806. Springer pp 184-190.
[16] Biere A, Cimatti AA, Clarke EM, Zhu Y (1999) Symbolic model checking without BDDs. In: Cleaveland R (ed) TACAS, Lecture Notes in Computer Science, vol 1579. Springer, pp 193-207.
[17] Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Miné A, Monniaux D, Rival X (2002) Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In: Mogensen TÆ, Schmidt DA, Sudborough IH (eds) The essence of computation, Lecture Notes in Computer Science, vol 2566. Springer, pp 85-108. · Zbl 1026.68514
[18] Brillout A, Kroening, D, Rümmer P, Wahl T (2010) An interpolating sequent calculus for quantifier-free Presburger arithmetic. In: Giesl H (ed) Proceedings of the 5th international joint conference on automated reasoning, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Lecture Notes in Computer Science, vol 6173. Springer, pp 384-399. · Zbl 1291.03112
[19] Bruttomesso R, Ghilardi S, Ranise S (2012) From strong amalgamability to modularity of quantifier-free interpolation. In: IJCAR, Lecture Notes in Computer Science. Springer, pp 118-133. · Zbl 1358.68183
[20] Bruttomesso R, Ghilardi S, Ranise S (2012) Quantifier-free interpolation of a theory of arrays. Logical Methods in Computer Science 8(2) · Zbl 1237.68123
[21] Bruttomesso R, Pek E, Sharygina N, Tsitovich A (2010) The OpenSMT solver. In: Esparza J, Majumdar R (eds) TACAS, Lecture Notes in Computer Science, vol 6015. Springer, pp 150-153.
[22] Carioni A, Ghilardi S, Ranise S (2011) Automated termination in model checking Modulo theories. In: Delzanno G, Potapov I (eds) RP, Lecture Notes in Computer Science, vol 6945. Springer, pp 110-124. · Zbl 1348.68124
[23] Chase DR, Wegman MN, Zadeck FK (1990) Analysis of pointers and structures. In: Fischer BN (ed) PLDI. ACM, pp 296-310.
[24] Cimatti A, Griggio A, Schaafsma BJ, Sebastiani R (2013) The MathSAT5 SMT solver. In: Piterman N, Smolka SA (eds) Proceedings of the 19th international conference on tools and algorithms for the construction and analysis of systems, TACAS 2013, held as part of the European joint conferences on theory and practice of software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Lecture Notes in Computer Science, vol 7795. Springer, pp 93-107. · Zbl 1105.68069
[25] Robert, Clarisó; Jordi, Cortadella, The octahedron abstract domain, Sci Comput Program, 64, 115-139, (2007) · Zbl 1171.68540
[26] Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: Allen Emerson E, Prasad Sistla A (eds) CAV, Lecture Notes in Computer Science, vol 1855. Springer, pp 154-169. · Zbl 0974.68517
[27] Clarke EM, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. In Jensen K, Podelski A (eds) TACAS, Lecture Notes in Computer Science, vol 2988. Springer, pp 168-176. · Zbl 1126.68470
[28] Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham RM, Harrison MA, Sethi R (eds) POPL. ACM, pp 238-252
[29] Cousot P, Cousot R, Logozzo F (2011) A parametric segmentation functor for fully automatic and scalable array content analysis. In Ball T, Sagiv M (eds) POPL. ACM, pp 105-118. · Zbl 1284.68210
[30] Cousot P, Halbwachs N (1978) Automatic discovery of linear restraints among variables of a program. In: Aho Alfred V, Zilles Stephen N, Szymanski Thomas G (eds) POPL. ACM Press, pp 84-96.
[31] Craig, W, Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory, J Symb Log, 22, 269-285, (1957) · Zbl 0079.24502
[32] Mendonça de Moura L, Bjørner N (2007) Efficient e-matching for SMT solvers. In Pfenning F (ed) CADE, Lecture Notes in Computer Science, vol 4603. Springer, pp 183-198. · Zbl 1213.68578
[33] Mendonça de Moura L, Bjørner N (2008) Z3: an efficient SMT solver. In: Ramakrishnan CR, Rehof J (eds) Proceedings of the 14th international conference on tools and algorithms for the construction and analysis of systems, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008, Lecture Notes in Computer Science, vol 4963. Springer, pp 337-340. · Zbl 0856.68096
[34] Delzanno, G; Esparza, J; Podelski, A, Constraint-based analysis of broadcast protocols, Proceedings of CSL, LNCS, 1683, 50-66, (1999) · Zbl 0944.68139
[35] Dillig I, Dillig T, Alex Aiken T (2010) Fluid updates: beyond strong vs. weak updates. In Gordon AD (ed), ESOP, Lecture Notes in Computer Science, vol 6012. Springer, pp 246-266. · Zbl 1260.68092
[36] Dimitrova R, Podelski A (2008) Is lazy abstraction a decision procedure for broadcast protocols? In: Logozzo F, Peled D, Zuck LD (eds) VMCAI, Lecture Notes in Computer Science, vol. 4905. Springer, pp 98-111. · Zbl 1138.68445
[37] Dudka K, Peringer P, Vojnar T (2011) Predator: a practical tool for checking manipulation of dynamic data structures using separation logic. In: Gopalakrishnan G, Qadeer S (eds) Proceedings of the 23rd international conference on computer aided verification, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Lecture Notes in Computer Science, vol 6806. Springer, pp 372-378.
[38] Dudka K, Peringer P, Vojnar T (2013) Byte-precise verification of low-level list manipulation. In: Logozzo F, Fähndrich M (eds) SAS, Lecture Notes in Computer Science, vol 7935. Springer, pp 215-237.
[39] Enderton HB (2001) A Mathematical introduction to logic. Elsevier Science. · Zbl 0992.03001
[40] Fähndrich M, Logozzo F (2010) Static contract checking with abstract interpretation. In Beckert B, Marché C (eds) FoVeOOS, Lecture Notes in Computer Science, vol 6528. Springer, pp 10-30. · Zbl 1308.68033
[41] Flanagan C, Qadeer S (2002) Predicate abstraction for software verification. In: Launchbury J, Mitchell JC (eds) Conference record of POPL 2002: the 29th SIGPLAN-SIGACT symposium on principles of programming languages, Portland, OR, USA, January 16-18, 2002. ACM, pp 191-202. · Zbl 1323.68371
[42] Furia C.A., Meyer B. (2010). Inferring loop invariants using postconditions. In A. Blass, N. Dershowitz, and W. Reisig (eds), Fields of Logic and Computation, volume 6300 of Lecture Notes in Computer Science, pages 277-300. Springer. · Zbl 1287.68108
[43] Ge, Y; Barrett, CW; Tinelli, C, Solving quantified verification conditions using satisfiability modulo theories, Ann. Math. Artif. Intell., 55, 101-122, (2009) · Zbl 1184.68461
[44] Ge Y, Mendonça de Moura L (2009) Complete instantiation for quantified formulas in Satisfiabiliby Modulo Theories. In Bouajjani A, Maler O (eds) CAV, Lecture Notes in Computer Science, vol 5643. Springer, pp 306-320. · Zbl 1242.68280
[45] Ghilardi S, Ranise S (2009) Model checking Modulo theory at work: the integration of Yices in MCMT. In: AFM.
[46] Ghilardi S, Ranise S (2010) Backward reachability of array-based systems by SMT solving: termination and invariant synthesis. Logical Methods in Computer Science 6(4) · Zbl 1213.68379
[47] Ghilardi S, Ranise S (2010) Mcmt: a model checker modulo theories. In Giesl J, Hähnle R (eds) Proceedings of the 5th international joint conference on automated reasoning, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Lecture Notes in Computer Science, vol 6173. Springer, pp 22-29. · Zbl 1291.68257
[48] Ghilardi, S; Ranise, S; Valsecchi, T, Light-weight SMT-based model checking, Electron Notes Theor Comput Sci, 250, 85-102, (2009) · Zbl 1335.68138
[49] Gopan D, Reps TW, Sagiv S (2005) A framework for numeric analysis of array operations. In: Palsberg J, Abadi M (eds) POPL. ACM, pp 338-350. · Zbl 1369.68138
[50] Graf S, Saïdi H (1997) Construction of abstract state graphs with PVS. In Grumberg O (ed) CAV, Lecture Notes in Computer Science, vol 1254. Springer, pp 72-83.
[51] Gulwani S, Tiwari A (2006) Combining abstract interpreters. In: Schwartzbach MI, Ball T (eds) PLDI. ACM, pp 376-386.
[52] Halbwachs N, Péron M (2008) Discovering properties about arrays in simple programs. In Gupta R, Amarasinghe SP (eds) PLDI. ACM, pp 339-348.
[53] Henzinger TA, Jhala R, Majumdar R, McMillan KL (2004) Abstractions from proofs. In: Jones ND, Leroy X (eds) POPL. ACM, pp 232-244. · Zbl 1325.68147
[54] Henzinger TA, Jhala R, Majumdar R, Sutre G (2002) Lazy abstraction. In: Launchbury J, Mitchell JC (eds) Conference record of POPL 2002: the 29th SIGPLAN-SIGACT symposium on principles of programming languages, Portland, OR, USA, January 16-18, 2002. ACM, pp 58-70. · Zbl 1323.68374
[55] Hind M (2001) Pointer analysis: haven’t we solved this problem yet? In: Field J, Snelting G (eds) PASTE. ACM, pp 54-61.
[56] Hoder K, Kovács L, Voronkov A (2010) Interpolation and symbol elimination in Vampire. In: Giesl H (ed) Proceedings of the 5th international joint conference on automated reasoning, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Lecture Notes in Computer Science, vol 6173. Springer, pp 188-195. · Zbl 1291.68348
[57] Hodges W (1993) Model theory, volume 42 of encyclopedia of mathematics and its applications. Cambridge University Press, Cambridge. · Zbl 0856.68096
[58] Jhala R, McMillan KL (2006) A practical and complete approach to predicate refinement. In: Hermanns H, Palsberg J (eds) TACAS, Lecture Notes in Computer Science, vol 3920. Springer, pp 459-473. · Zbl 1180.68118
[59] Jhala R, McMillan KL (2007) Array abstractions from proofs. In Damm W, Hermanns H (eds) CAV, Lecture Notes in Computer Science, vol 4590. Springer, pp 193-206. · Zbl 1135.68474
[60] Kapur D, Majumdar R, Zarba CG (2006) Interpolation for data structures. In: Young M, Devanbu PT (eds) SIGSOFT FSE. ACM, pp 105-116.
[61] Kovács L, Voronkov A (2009) Finding loop invariants for programs over arrays using a theorem prover. In Chechik M, Wirsing M (eds) FASE, Lecture Notes in Computer Science, vol 5503. Springer, pp 470-485.
[62] Lahiri SK, Bryant RE (2004) Constructing quantified invariants via predicate abstraction. In Steffen B, Levi G (eds) VMCAI, Lecture Notes in Computer Science, vol 2937. Springer, pp 267-281. · Zbl 1202.68251
[63] Lahiri SK, Bryant RE (2004) Indexed predicate discovery for unbounded system verification. In Alur R, Peled D (eds) CAV, Lecture Notes in Computer Science, vol. 3114. Springer, pp 135-147. · Zbl 1103.68627
[64] Larraz D, Rodríguez-Carbonell E, Rubio A (2013) SMT-based array invariant generation. In: Giacobazzi R, Berdine J, Mastroeni I (eds) VMCAI, Lecture Notes in Computer Science, vol 7737. Springer, pp 169-188. · Zbl 1426.68056
[65] Manna Z, Pnueli A (1992) The temporal logic of reactive and concurrent systems-specification. Springer, Berlin · Zbl 0753.68003
[66] McCarthy J (1962) Towards a mathematical science of computation. In: IFIP Congress, pp 21-28.
[67] McMillan KL (2006) Lazy abstraction with interpolants. In: Ball T, Jones RB (eds) Proceedings of the 18th international conference on computer aided verification, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Lecture Notes in Computer Science, vol 4144. Springer, pp 123-136. · Zbl 1188.68196
[68] McMillan KL (2008) Quantified invariant generation using an interpolating saturation prover. In Ramakrishnan CR, Rehof J (eds) Proceedings of the 14th international conference on tools and algorithms for the construction and analysis of systems, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March-April 6, 2008, Lecture Notes in omputer Science, vol 4963. Springer, pp 413-427.
[69] Antoine, Miné, The octagon abstract domain, Higher-Order Symb Comput, 19, 31-100, (2006) · Zbl 1105.68069
[70] Nelson, G; Oppen, DC, Simplification by cooperating decision procedures, ACM Trans Program Lang Syst, 1, 245-257, (1979) · Zbl 0452.68013
[71] Podelski A, Wies T (2005) Boolean heaps. In Hankin C, Siveroni I (eds) SAS, Lecture Notes in Computer Science, vol 3672. Springer, pp 268-283. · Zbl 1141.68374
[72] Ranise S, Tinelli C (2006). The satisfiability Modulo theories library (SMT-LIB). http://www.smt-lib.orgwww.SMT-LIB.org
[73] Reynolds JC (2002) Separation logic: a logic for shared mutable data structures. In: LICS. IEEE Computer Society, pp 55-74.
[74] Rümmer P, Subotić P (2013) Exploring interpolants. In: Jobstmann B, Ray S (eds) FMCAD. FMCAD Inc., pp 69-76.
[75] Sagiv S, Reps TW, Reinhard Wilhelm. Parametric shape analysis via 3-valued logic. In: Appel AW, Aiken A (eds) POPL. ACM, pp 105-118 (1999).
[76] Seghir MN, Podelski A, Wies T (2009) Abstraction refinement for quantified array assertions. In: Palsberg J, Su Z (eds) SAS, Lecture Notes in Computer Science, vol 5673. Springer, pp 3-18. · Zbl 1248.68151
[77] Srivastava S, Gulwani S (2009) Program verification using templates over predicate abstraction. In: Hind M, Diwan A (eds) PLDI. ACM, pp 223-234.
[78] Wirth N (1978) Algorithms + data structures = programs. Prentice-Hall Series in Automatic Computation, Pearson Education
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.