Program Verification using Constraint Handling Rules and Array Constraint Generalizations

• Autorzy: De Angelis E. , Fioravanti F. , Pettorossi A. , Proietti M.

Identyfikatory

DOI

10.3233/FI-2017-1461

• Języki publikacji: EN

Abstrakty

EN

The transformation of constraint logic programs (CLP programs) has been shown to be an effective methodology for verifying properties of imperative programs. By following this methodology, we encode the negation of a partial correctness property of an imperative program prog as a predicate incorrect defined by a CLP program T, and we show that prog is correct by transforming T into the empty program (and thus incorrect does not hold) through the application of semantics preserving transformation rules. We can also show that prog is incorrect by transforming T into a program with the fact incorrect (and thus incorrect does hold). Some of the transformation rules perform replacements of constraints that are based on properties of the data structures manipulated by the program prog. In this paper we show that Constraint Handling Rules (CHR) are a suitable formalism for representing and applying constraint replacements during the transformation of CLP programs. In particular, we consider programs that manipulate integer arrays and we present a CHR encoding of a constraint replacement strategy based on the theory of arrays. We also propose a novel generalization strategy for constraints on integer arrays that combines CHR constraint replacements with various generalization operators on integer constraints, such as widening and convex hull. Generalization is controlled by additional constraints that relate the variable identifiers in the imperative program prog and the CLP representation of their values. The method presented in this paper has been implemented and we have demonstrated its effectiveness on a set of benchmark programs taken from the literature.

Słowa kluczowe

EN

Constraint Handling Rules; CHR; constraint logic programming; CLP; program transformation; program verification

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2017
• Tom: Vol. 150, nr 1
• Strony: 73--117
• Opis fizyczny: Bibliogr. 49 poz., rys., tab.

Twórcy

autor

De Angelis E.

• University of Chieti-Pescara, Viale Pindaro 42, 65127, Pescara, Italy

autor

Fioravanti F.

• University of Chieti-Pescara, Viale Pindaro 42, 65127, Pescara, Italy

autor

Pettorossi A.

• University of Rome Tor Vergata, Via del Politecnico 1, 00133 Rome, Italy

autor

Proietti M.

• IASI-CNR, Via dei Taurini 19, 00185 Rome, Italy

Bibliografia

• [1] Peralta JC, Gallagher JP, and Saglam H. Analysis of imperative programs through analysis of constraint logic programs. In Proc. SAS ’98, LNCS 1503, pages 246-261. Springer, 1998. doi: 10.1007/3-540-49727-7_15.
• [2] De Angelis E, Fioravanti F, Pettorossi A, and Proietti M. Program verification via iterated specialization. Science of Computer Programming, 95, Part 2: 149-175, 2014. doi: 10.1016/j.scico.2014.05.017.
• [3] Winskel G. The Formal Semantics of Programming Languages: An Introduction. The MIT Press, Cambridge, Massachusetts. 1993. ISBN: 0-262-23169-7.
• [4] Cousot P, and Cousot R. Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixpoints. In Proc. POPL’77, pages 238-252. ACM, 1977. doi: 10.1145/512950.512973.
• [5] Albert E, Gómez-Zamalloa M, Hubert L, and Puebla G. Verification of Java bytecode using analysis and transformation of logic programs. In Proc. PADL’07, LNCS 4354, pages 124-139. Springer, 2007. doi: 10.1007/978-3-540-69611-7_8.
• [6] Kafle B, and Gallagher JP. Constraint Specialisation in Horn Clause Verification. In Proc. PEPM’15 pages 85-90. ACM, 2015. doi: 10.1145/2678015.2682544.
• [7] Méndez-Lojo M, Navas JA, and Hermenegildo MV. A flexible, (C)LP-based approach to the analysis of object-oriented programs. In Proc. LOPSTR'07, LNCS 4915, pages 154-168. Springer, 2008, doi: 10.1007/978-3-540-78769-3_11.
• [8] Duck GJ. Jaffar J, and Koh NCH. Constraint-based program reasoning with heaps and separation. In Proc. CP’13, LNCS 8124, pages 282-298. Springer, 2013. doi: 10.1007/978-3-642-40627-0_24.
• [9] Flanagan C. Automatic software model checking via constraint logic. Science of Computer Programming, 2004; 50 (l-3): 253-270. doi: 10.1016/j.scico.2004.01.006.
• [10] Jaffar J, Santosa A, and Voicu R. An interpolation method for CLP traversal. In Proc. CP’09, LNCS 5732, pages 454-469. Springer, 2009. doi: 10.1007/978-3-642-04244-7_37.
• [11] Bjørner N, McMillan K, and Rybalchenko A. Program verification as satisfiability modulo theories. In Proc. SMT-COMP’12, EPiC Series, vol. 20, pages 3-11, 2013. http://www.easychair.org/publications/download/Program_Verification_as_Satisfiability_Modulo_Theories.
• [12] de Moura LM, and Bjørner N. Z3: An efficient SMT solver. In Proc. TACAS’08, LNCS 4963. 337-340. Springer, 2008. doi: 10.1007/978-3-540-78800-3_24.
• [13] Grebenshchikov S, Gupta A, Lopes NP, Popeea C, and Rybalchenko A. HSF(C): A software verifier based on Horn clauses. In Proc. TACAS’12, LNCS 7214, pages 549-551. Springer, 2012. doi: 10.1007/978-3-642-28756-5_46.
• [14] Podelski A, and Rybalchenko A. ARMC: The logical choice for software model checking with abstraction refinement. In Proc. PADL’07, LNCS 4354, pages 245-259. Springer, 2007. doi: 10.1007/978-3-540-69611-7_16.
• [15] Rümmer P, Hojjat H, and Kuncak V. Disjunctive interpolants for Horn-clause verification. In Proc. CAV’13, LNCS 8044, pages 347-363. Springer, 2013. doi: 10.1007/978-3-642-39799-8_24.
• [16] Etalle S, and Gabbrielli M. Transformations of CLP modules. Theoretical Computer Science, 1996; 166: 101-146. doi: 10.1016/0304-3975(95)00148-4.
• [17] Fioravanti F, Pettorossi A, and Proietti M. Transformation rules for locally stratified constraint logic programs. In K.-K. Lau and M. Bruynooghe, editors, Program Development in Computational Logic. LNCS 3049, pages 292-340. Springer, 2004. doi: 10.1007/978-3-540-25951-0_10.
• [18] Pettorossi A, and Proietti M. Transformation of logic programs: Foundations and techniques. Journal of Logic Programming, 1994; 19 (20): 261-320. doi: 10.1016/0743-1066(94)90028-0.
• [19] De Angelis E, Fioravanti F, Pettorossi A, and Proietti M. A rule-based verification strategy for array manipulating programs. Fundamenta Informaticae, 2015; 140 (3-4): 329-355. doi: 10.3233/FT-2015-1257.
• [20] Frühwirth T. Theory and practice of Constraint Handling Rules. Journal of Logic Programming, 1998; 37 (1-3): 95-138. doi: 10.1016/S0743-1066(98)10005-5.
• [21] Bradley AR, Manna Z, and Sipma HB. What’s decidable about arrays? In Proc. VMCAI’06, LNCS 3855, pages 427-442. Springer, 2006. doi: 10.1007/11609773_28.
• [22] Cousot P, and Halbwachs N. Automatic discovery of linear restraints among variables of a program. In: Proc. POPL’78, pages 84-96. ACM, 1978. doi: 10.1145/512760.512770.
• [23] De Angelis E, Fioravanti F, Pettorossi A, and Proietti M. VeriMAP: A tool for verifying programs through transformations. In Proc. TACAS’14, LNCS 8413, pages 568-574. Springer, 2014. Available at: http://www.map.uniroma2.it/VeriMAP. doi: 10.1007/978-3-642-54862-8_47.
• [24] Lloyd JW. Foundations of Logic Programming. Springer-Verlag, Berlin, 1987. Second Edition. ISBN: 3-540-18199-7.
• [25] Jaffar J, Maher M, Marriott K, and Stuckey P. The semantics of constraint logic programming. Journal of Logic Programming, 1998; 37: 1-46. doi: 10.1016/S0743-1066(98)10002-X.
• [26] Reynolds CJ. Theories of Programming Languages. Cambridge University Press, 1998. ISBN: 9780521594141.
• [27] De Angelis E, Fioravanti F, Pettorossi A, and Proietti M. Proving correctness of imperative programs by linearizing constrained Horn clauses. Theory and Practice of Logic Programming, 2015; 15 (4-5): 635-650. doi: 10.1017/S1471068415000289.
• [28] Abdennadher S, and Schütz H. CHRV: A flexible query language. In Proc. FQAS’98, LNCS 1495, pages 1-14. Springer, 1998. doi: 10.1007/BFb0055987.
• [29] Fioravanti F, Pettorossi A, Proietti M, and Senni V. Generalization strategies for the verification of infinite state systems. Theory and Practice of Logic Programming, 2013; 13 (2): 175-199. doi: 10.1017/S1471068411000627.
• [30] Leuschel M. On the power of homeomorphic embedding for online termination. In Proc. SAS’98, LNCS 1503, pages 230-245. Springer, 1998. doi: 10.1007/3-540-49727-7_14.
• [31] Peralta JC, and Gallagher JP. Convex hull abstractions in specialization of CLP programs. In Proc. LOP-STR’02, LNCS 2664, pages 90-108. Springer, 2003. doi: 10.1007/3-540-45013-0_8.
• [32] Necula GC, McPeak S, Rahul SP, and Weimer W. CIL: Intermediate language and tools for analysis and transformation of C programs. In Proc. CC’02, LNCS 2304, pages 209-265. Springer, 2002. doi: 10.1007/3-540-45937-5_16.
• [33] Bjømer N, McMillan K, and Rybalchenko A. On solving universally quantified Horn clauses. In Proc. SAS’13, LNCS 7935, pages 105-125. Springer, 2013. doi: 10.1007/978-3-642-38856-9_8.
• [34] Cousot P, Cousot R, and Logozzo F. A parametric segmentation functor for fully automatic and scalable array content analysis. In Proc. POPL’11, pages 105-118. ACM, 2011. doi: 10.1145/1926385.1926399.
• [35] Dillig I, Dillig T, and Aiken A. Fluid updates: Beyond strong vs. weak updates. In Proc. ESOP’10, LNCS 6012, pages 246-266. Springer, 2010. doi: 10.1007/978-3-642-11957-6_14.
• [36] Halbwachs N, and Péron M. Discovering properties about arrays in simple programs. In Proc. PLDI’08, pages 339-348. ACM, 2008. doi: 10.1145/1379022.1375623.
• [37] Larraz D, Rodríguez-Carbonell E, and Rubio A. SMT-based array invariant generation. In Proc. VMCAI’13, LNCS 7737, pages 169-188. Springer, 2013. doi: 10.1007/978-3-642-35873-9_12.
• [38] Gopan D, Reps TW, and Sagiv S. A framework for numeric analysis of array operations. In Proc. POPL’05, pages 338-350. ACM, 2005. doi: 10.1145/1040305.1040333.
• [39] Flanagan C, and Qadeer S. Predicate abstraction for software verification. In Proc. POPL’02, pages 191-202. ACM, 2002. doi: 10.1145/565816.503291.
• [40] Lahiri SK, and Bryant RE. Predicate abstraction with indexed predicates. ACM Transactions on Computational Logic, 2007; 9 (1). doi: 10.1145/1297658.1297662.
• [41] Gulavani BS, Chakraborty S, Nori AV, and Rajamani SK. Automatically refining abstract interpretation In Proc. TACAS’08, LNCS 4963, pages 443-458. Springer, 2008. doi: 10.1007/978-3-540-78800-3_33.
• [42] Seghir MN, Podelski A, and Wies T. Abstraction refinement for quantified array assertions. In Proc. SAS’09, LNCS 5673, pages 3-18. Springer, 2009. doi: 10.1007/978-3-642-03237-0_3.
• [43] Jhala R, and McMillan KL. Array abstractions from proofs. In Proc. CAV’07, LNCS 4590, pages 193—206. Springer, 2007. doi: 10.1007/978-3-540-73368-3_23.
• [44] Kovács L, and Voronkov A. Finding loop invariants for programs over arrays using a theorem prover. In Proc. FASE’09, LNCS 5503, pages 470-485. Springer, 2009. doi: 10.1007/978-3-642-00593-0_33.
• [45] McMillan KL. Quantified invariant generation using an interpolating saturation prover. In Proc. TACAS’08, LNCS 4963, pages 413-427. Springer, 2008. doi: 10.1007/978-3-540-78800-3_31.
• [46] Alberti F, Bruttomesso R, Ghilardi S, Ranise S, and Sharygina N. SAFARI: SMT-based abstraction for arrays with interpolants. In Proc. CAV’12, LNCS 7358, pages 679-685. Springer, 2012. doi: 10.1007/978-3-642-31424-7_49.
• [47] Alberti F, Ghilardi S, and Sharygina N. Decision procedures for flat array properties. In Proc. TACAS'14. LNCS 8413, pages 15-30. Springer, 2014. doi: 10.1007/978-3-642-54862-8_2.
• [48] De Angelis E, Fioravanti F, Pettorossi A, and Proietti M. Semantics-based generation of verification conditions by program specialization. In Proc. PPDP’15, pages 91-102. ACM, 2015. doi: 10.1145/2790449.2790529.
• [49] Huet G. Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of ACM, 1980; 27 (4): 797-821. doi: 10.1145/322217.322230.

Uwagi

Opracowanie ze środków MNiSW w ramach umowy 812/P-DUN/2016 na działalność upowszechniającą naukę (zadania 2017).