A Rule-based Verification Strategy for Array Manipulating Programs

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

Identyfikatory

DOI

10.3233/FI-2015-1257

• Konferencja: Italian Conference on Computational Logic, CILC 2013, (25-27.09.2013; Catania, Italy)
• Języki publikacji: EN

Abstrakty

EN

We present a method for verifying properties of imperative programs that manipulate integer arrays. Imperative programs and their properties are represented by using Constraint Logic Programs (CLP) over integer arrays. Our method is refutational. Given a Hoare triple {ϕ} prog {ψ} that defines a partial correctness property of an imperative program prog, we encode the negation of the property as a predicate incorrect defined by a CLP program P, and we show that the property holds by proving that incorrect is not a consequence of P. Program verification is performed by applying a sequence of semantics preserving transformation rules and deriving a new CLP program T such that incorrect is a consequence of P iff it is a consequence of T . The rules are applied according to an automatic strategy whose objective is to derive a program T that satisfies one of the following properties: either (i) T is the empty set of clauses, hence proving that incorrect does not hold and prog is correct, or (ii) T contains the fact incorrect, hence proving that prog is incorrect. Our transformation strategy makes use of an axiomatization of the theory of arrays for the manipulation of array constraints, and also applies the widening and convex hull operators for the generalization of linear integer constraints. The strategy has been implemented in the VeriMAP transformation system and it has been shown to be quite effective and efficient on a set of benchmark array programs taken from the literature.

Słowa kluczowe

EN

logic programming; constraint logic programs; CLP; verification; quadratic transformations; refutation logic

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2015
• Tom: Vol. 140, nr 3/4
• Strony: 329--355
• Opis fizyczny: Bibliogr. 50 poz., 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, Viale Manzoni 30, 00185 Rome, Italy

Bibliografia

• [1] E. Albert, M. Gómez-Zamalloa, L. Hubert, and G. Puebla. Verification of Java bytecode using analysis and transformation of logic programs. Proc. PADL ’07, LNCS 4354, pages 124–139. Springer, 2007.
• [2] F. Alberti, S. Ghilardi, and N. Sharygina. Decision Procedures for Flat Array Properties. In TACAS ’14, LNCS 8413, pages 15–30. Springer, 2014.
• [3] F. Alberti, S. Ghilardi, and N. Sharygina. BOOSTER: An Acceleration-Based Verification Framework for Array Programs. In ATVA ’14, LNCS 8837, pages 18–23. Springer, 2014.
• [4] N. Bjørner, K. McMillan, and A. Rybalchenko. Program verification as satisfiability modulo theories. In SMT ’12, pages 3–11, 2012.
• [5] N. Bjørner, K. McMillan, and A. Rybalchenko. On solving universally quantified Horn clauses. In SAS ’13, LNCS 7395, pages 105–125. Springer, 2013.
• [6] A. R. Bradley, Z. Manna, and H. B. Sipma. What’s decidable about arrays? In VMCAI ’06, LNCS 3855, pages 427–442. Springer, 2006.
• [7] P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixpoints. In POPL ’77, pages 238–252. ACM, 1977.
• [8] P. Cousot, R. Cousot, and F. Logozzo. A parametric segmentation functor for fully automatic and scalable array content analysis. In POPL ’11, pages 105–118, ACM, 2011.
• [9] P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In POPL ’78, pages 84–96, ACM, 1978.
• [10] E. De Angelis, F. Fioravanti, A. Pettorossi, and M. Proietti. Verifying Array Programs by Transforming Verification Conditions. In VMCAI ’14, LNCS 8318, pages 182–202. Springer, 2014.
• [11] E. De Angelis, F. Fioravanti, A. Pettorossi, and M. Proietti. VeriMAP: A Tool for Verifying Programs through Transformations. In TACAS ’14, LNCS 8413, pages 568–574. Springer, 2014.
• [12] E. De Angelis, F. Fioravanti, A. Pettorossi, and M. Proietti. Program verification via iterated specialization. Science of Computer Programming, 95, Part 2:149–175, 2014.
• [13] I. Dillig, T. Dillig, and A. Aiken. Fluid updates: beyond strong vs. weak updates. In ESOP’10, LNCS 6012, pages 246–266. Springer, 2010.
• [14] G. J. Duck, J. Jaffar, and N. C. H. Koh. Constraint-based program reasoning with heaps and separation. In CP ’13, LNCS 8124, pages 282–298. Springer, 2013.
• [15] S. Etalle and M. Gabbrielli. Transformations of CLP modules. Theor. Comput. Sci., 166:101–146, 1996.
• [16] F. Fioravanti, A. Pettorossi,M. Proietti, and V. Senni. Improving reachability analysis of infinite state systems by specialization. Fundamenta Informaticae, 119(3-4):281–300, 2012.
• [17] F. Fioravanti, A. Pettorossi, M. Proietti, and V. Senni. Generalization strategies for the verification of infinite state systems. Theory and Practice of Logic Programming, 13(2):175–199, 2013.
• [18] C. Flanagan. Automatic software model checking via constraint logic. In Sci. Comput. Program., 50(1–3):253–270, 2004.
• [19] C. Flanagan and S. Qadeer. Predicate abstraction for software verification. In POPL ’02, pages 191–202, New York, NY, USA, 2002. ACM.
• [20] S. Ghilardi, E. Nicolini, S. Ranise, and D. Zucchelli. Decision procedures for extensions of the theory of arrays. Ann. Math. Artif. Intell., 50(3-4):231–254, 2007.
• [21] S. Ghilardi and S. Ranise. MCMT: AModel CheckerModulo Theories. Proc. IJCAR ’10, LNCS 6173, pages 22–29. Springer, 2010.
• [22] D. Gopan, T. W. Reps, and S. Sagiv. A framework for numeric analysis of array operations. In POPL ’05, pages 338–350. ACM, 2005.
• [23] S. Grebenshchikov, A. Gupta, N. P. Lopes, C. Popeea, and A. Rybalchenko. HSF(C): A Software Verifier based on Horn Clauses. In TACAS ’12, LNCS 7214, pages 549–551. Springer, 2012.
• [24] B. S. Gulavani, S. Chakraborty, A. V. Nori, and S. K. Rajamani. Automatically Refining Abstract Interpretations. In TACAS ’08, LNCS 4963, pages 443–458. Springer, 2008.
• [25] N. Halbwachs and M. Péron. Discovering properties about arrays in simple programs. In PLDI ’08, pages 339–348, 2008.
• [26] A. Haran and M. Carter and M. Emmi and A. Lal and S. Qadeer and Z. Rakamari´c. SMACK+Corral: A Modular Verifier. In TACAS ’15, LNCS 9035, pages 451–454. Springer, 2015.
• [27] K. S. Henriksen and J. P. Gallagher. Abstract interpretation of PIC programs through logic programming. Proc. SCAM ’06, pages 103 – 179, 2006.
• [28] G. Huet andD. C. Oppen. Equations and Rewrite Rules: A Survey. In Formal Language Theory: Perspectives and Open Problems, Academic Press, 1980.
• [29] J. Jaffar andM.Maher. Constraint logic programming: A survey. Journal of Logic Programming, 19/20:503–581, 1994.
• [30] J. Jaffar, J. A. Navas, and A. E. Santosa. TRACER: A Symbolic Execution Tool for Verification. In CAV ’12, LNCS 7358, pages 758–766. Springer, 2012.
• [31] J. Jaffar, A. Santosa, and R. Voicu. An interpolation method for CLP traversal. In CP ’09, LNCS 5732, pages 454–469. Springer, 2009.
• [32] R. Jhala and K. L. McMillan. Array abstractions from proofs. In CAV ’07, LNCS 4590, pages 193–206, 2007.
• [33] L. Kovács and A. Voronkov. Finding loop invariants for programs over arrays using a theorem prover. In FASE ’09, LNCS 5503, pages 470–485. Springer, 2009.
• [34] S. K. Lahiri and R. E. Bryant. Predicate abstraction with indexed predicates. ACM Trans. Comput. Log., 9(1), 2007.
• [35] A. Lalh, S. Qadeer and S. K. Lahiri. A Solver for Reachability Modulo Theories. In CAV ’12, LNCS 7358, pages 427–443, 2012.
• [36] D. Larraz, E. Rodríguez-Carbonell, and A. Rubio. SMT-based array invariant generation. In VMCAI ’13, LNCS 7737, pages 169–188. Springer, 2013.
• [37] K. Rustan M. Leino. This is Boogie 2. http://research.microsoft.com/apps/pubs/default.aspx?id=147643, 2008.
• [38] J. W. Lloyd. Foundations of Logic Programming. Springer-Verlag, Berlin, 1987. Second Edition.
• [39] J. McCarthy. Towards a mathematical science of computation. In C.M. Popplewell, editor, Information Processing: Proceedings of IFIP 1962, pages 21–28, Amsterdam, 1963. North Holland.
• [40] K. L. McMillan. Quantified invariant generation using an interpolating saturation prover. In TACAS ’08, LNCS 4963, pages 413–427, 2008.
• [41] M. Méndez-Lojo, J. A. Navas, and M. V. Hermenegildo. A flexible, (C)LP-based approach to the analysis of object-oriented programs. Proc. LOPSTR ’07, LNCS 4915, pages 154–168. Springer, 2008.
• [42] G. C. Necula, S. McPeak, S. P. Rahul, andW. Weimer. CIL: Intermediate language and tools for analysis and transformation of C programs. In Compiler Construction, LNCS 2304, pages 209–265. Springer, 2002.
• [43] J. C. Peralta and J. P. Gallagher. Convex hull abstractions in specialization of CLP programs. In LOPSTR ’02, LNCS 2664, pages 90–108. Springer, 2003.
• [44] J. C. Peralta, J. P. Gallagher, and H. Saglam. Analysis of Imperative Programs through Analysis of Constraint Logic Programs. In SAS ’98, LNCS 1503, pages 246–261. Springer, 1998.
• [45] A. Pettorossi and M. Proietti. Transformation of Logic Programs: Foundations and Techniques. In Journal of Logic Programming, Vol. 19,20, pages 261–320, 1994.
• [46] A. Podelski and A. Rybalchenko. ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement. In PADL ’07, LNCS 4354, pages 245–259. Springer, 2007.
• [47] C. J. Reynolds. Theories of Programming Languages. Cambridge Univ.Press 1998.
• [48] P. Rümmer, H. Hojjat, and V. Kuncak. Disjunctive interpolants for Horn-clause verification. Proc. CAV ’13, LNCS 8044, pages 347–363. Springer, 2013.
• [49] M. N. Seghir, A. Podelski, and T. Wies. Abstraction refinement for quantified array assertions. In SAS ’09, LNCS 5673, pages 3–18. Springer, 2009.
• [50] G. Winskel. The Formal Semantics of Programming Languages: An Introduction. The MIT Press, 1993.