[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Cell Morphing: From Array Programs to Array-Free Horn Clauses

  • Conference paper
  • First Online:
Static Analysis (SAS 2016)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9837))

Included in the following conference series:

Abstract

Automatically verifying safety properties of programs is hard. Many approaches exist for verifying programs operating on Boolean and integer values (e.g. abstract interpretation, counterexample-guided abstraction refinement using interpolants), but transposing them to array properties has been fraught with difficulties. Our work addresses that issue with a powerful and flexible abstraction that morphes concrete array cells into a finite set of abstract ones. This abstraction is parametric both in precision and in the back-end analysis used.

From our programs with arrays, we generate nonlinear Horn clauses over scalar variables only, in a common format with clear and unambiguous logical semantics, for which there exist several solvers. We thus avoid the use of solvers operating over arrays, which are still very immature.

Experiments with our prototype vaphor show that this approach can prove automatically and without user annotations the functional correctness of several classical examples, including selection sort, bubble sort, insertion sort, as well as examples from literature on array analysis.

The research leading to these results has received funding from the European Research Council under the European Union’s Seventh Framework Programme (FP/2007-2013) / ERC Grant Agreement nr. 306595 “STATOR”.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
GBP 19.95
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
GBP 35.99
Price includes VAT (United Kingdom)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
GBP 44.99
Price includes VAT (United Kingdom)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    In the following, we shall lump as “scalar” operations all operations not involving the array under consideration, e.g. \(i:=i+1\). Any data types (integers, strings etc.) are supported if supported by the back-end solver.

  2. 2.

    With the exception of pointers and references, which need special handling and may be internally converted to array accesses.

  3. 3.

    A nonlinear clause is of the form \(P_1(\dots ) \wedge P_2(\dots ) \wedge \dots \wedge P_n(\dots ) \wedge \textit{arithmetic condition} \implies Q(\dots )\), with several antecedent predicates \(P_1, P_2, \dots \). Unfolding such rules yields a tree. In contrast a linear rule \(P(\dots ) \wedge \textit{arithmetic condition} \implies Q(\dots )\) has only one antecedent predicate, and unfolding a system of such rules yields a linear chain.

  4. 4.

    Z3 and Eldarica can also occasionally directly solve Horn clauses over arrays; we also compare to that.

  5. 5.

    Classically, we denote the sets using predicates: \(I_{i_0}(\mathbf {x})\) means \(\mathbf {x}\in I_{i_0}\).

  6. 6.

    https://github.com/Z3Prover hash 7f6ef0b6c0813f2e9e8f993d45722c0e5b99e152; due to various problems we preferred not to use results from later versions.

  7. 7.

    https://bitbucket.org/spacer/code hash 7e1f9af01b796750d9097b331bb66b752ea0ee3c.

  8. 8.

    https://github.com/uuverifiers/eldarica/releases/tag/v1.1-rc.

  9. 9.

    A classical approach is to add overflow checks to the intermediate representation of programs in order to be able to express their semantics with mathematical integers even though they operate over machine integers.

  10. 10.

    Some of these tools can however infer some simpler array invariants.

  11. 11.

    For instance, \(I_{loop}=loop(n,i,a)\), \(I_{end}=end(n,i,a)\).

  12. 12.

    also denoted by \(I^\sharp _\ell ((i,n),(k,a_k))\) for sake of readability.

  13. 13.

    If one is sure that the only relation that matters between a and b are between cells of same index, then one can use triples \((i,a_i,b_i)\).

  14. 14.

    It would still be possible to proceed by first analyzing the first loop, getting the scalar invariant at location , quantifying it universally as , then analyzing the second loop. Such an approach would however fail if this program was itself included in an outer loop.

  15. 15.

    The statement if tab[i]!=42 is decomposed into x:=a[i];if(x!=42).

  16. 16.

    In Example 8 we shall see how to prove that the multiset of elements in the output is the same as in the input.

  17. 17.

    Nontrivial in the sense that a human user operating a Floyd-Hoare proof assistant typically does not come up with them so easily.

  18. 18.

    http://smtlib.cs.uiowa.edu/.

  19. 19.

    We suspect that different choices in SAT lead to different proofs of unsatisfiability, thus different interpolants and different refinements in the PDR algorithm.

  20. 20.

    Their approach is not implemented in Z3 (personal communication from N. Bjørner).

References

  1. Alberti, F., Monniaux, D.: Polyhedra to the rescue of array interpolants. In: Symposium on applied computing (Software Verification & Testing), pp. 1745–1750. ACM (2015). doi:10.1145/2695664.2695784

  2. Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: An extension of lazy abstraction with interpolation for programs with arrays. Formal Methods Syst. Des. 45(1), 63–109 (2014). doi:10.1007/s10703-014-0209-9

    Article  MATH  Google Scholar 

  3. Bjørner, N., McMillan, K., Rybalchenko, A.: On solving universally quantified Horn clauses. In: Logozzo, F., Fähndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 105–125. Springer, Heidelberg (2013). doi:10.1145/2695664.2695784

    Chapter  Google Scholar 

  4. Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In: Mogensen, T.Æ., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol. 2566, pp. 85–108. Springer, Heidelberg (2002). doi:10.1007/3-540-36377-7_5

    Chapter  Google Scholar 

  5. Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Programming Language Design and Implementation (PLDI), pp. 196–207. ACM (2003). doi:10.1145/781131.781153

  6. Bornat, R.: Proving pointer programs in Hoare logic. In: Backhouse, R.C., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol. 1837, pp. 102–126. Springer, Heidelberg (2000). doi:10.1007/10722010_8

    Chapter  Google Scholar 

  7. Bozga, M., Habermehl, P., Iosif, R., Konečný, F., Vojnar, T.: Automatic verification of integer array programs. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 157–172. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02658-4_15

    Chapter  Google Scholar 

  8. Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427–442. Springer, Heidelberg (2006). doi:10.1007/11609773_28

    Chapter  Google Scholar 

  9. Christ, J.: Interpolation Modulo Theories. Ph.D thesis, University of Freiburg (2015)

    Google Scholar 

  10. Cornish, J.R.M., Gange, G., Navas, J.A., Schachte, P., Søndergaard, H., Stuckey, P.J.: Analyzing array manipulating programs by program transformation. In: Proietti, M., Seki, H. (eds.) LOPSTR 2014. LNCS, vol. 8981, pp. 3–20. Springer, Heidelberg (2015). doi:10.1007/978-3-319-17822-6_1

    Google Scholar 

  11. Cousot, P., Cousot, R.: Abstract interpretation frameworks. J. Log. Comput. 2(4), 511–547 (1992). doi:10.1093/logcom/2.4.511

    Article  MathSciNet  MATH  Google Scholar 

  12. Cousot, P., Cousot, R., Logozzo, F.: A parametric segmentation functor for fully automatic and scalable array content analysis. In: Principles of Programming Languages (POPL), pp. 105–118. ACM (2011). doi:10.1145/1926385.1926399

  13. Cousot, P., Cousot, R.: Invited talk: higher order abstract interpretation. In: IEEE International Conference on Computer Languages, pp. 95–112. IEEE (1994)

    Google Scholar 

  14. De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: A rule-based verification strategy for array manipulating programs. Fundamenta Informaticae 140(3–4), 329–355 (2015). doi:10.3233/FI-2015-1257

    Article  MathSciNet  MATH  Google Scholar 

  15. Dillig, I., Dillig, T., Aiken, A.: Fluid updates: beyond strong vs. weak updates. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 246–266. Springer, Heidelberg (2010). doi:10.1007/978-3-642-11957-6_14

    Chapter  Google Scholar 

  16. Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: POPL, pp. 191–202 (2002)

    Google Scholar 

  17. Gopan, D., Reps, T.W., Sagiv, S.: A framework for numeric analysis of array operations. In: Principles of Programming Languages (POPL), pp. 338–350 (2005) doi:10.1145/1040305.1040333

  18. Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The seahorn verification framework. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343–361. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

  19. Halbwachs, N., Péron, M.: Discovering properties about arrays in simple programs. In: Programming language design and implementation (PLDI), pp. 339–348. ACM (2008) doi:10.1145/1375581.1375623

  20. Halpern, J.Y.: Presburger arithmetic with unary predicates is \(\Pi ^1_1\) complete. J. Symbolic Logic 56(2), 637–642 (1991). doi:10.2307/2274706. ISSN 0022–4812

    Article  MathSciNet  MATH  Google Scholar 

  21. Henry, J., Monniaux, D., Moy, M.: Succinct representations for abstract interpretation. In: Miné, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 283–299. Springer, Heidelberg (2012). doi:10.1007/978-3-642-33125-1_20

    Chapter  Google Scholar 

  22. Hoder, K., Bjørner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 157–171. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31612-8_13. ISBN 978-3-642-31611-1

    Chapter  Google Scholar 

  23. Jhala, R., McMillan, K.L.: Array abstractions from proofs. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 193–206. Springer, Heidelberg (2007). doi:10.1007/978-3-540-73368-3_23

    Chapter  Google Scholar 

  24. Komuravelli, A., Gurfinkel, A., Chaki, S., Clarke, E.M.: Automatic abstraction in SMT-based unbounded software model checking. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 846–862. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39799-8_59. ISBN 978-3-642-39798-1

    Chapter  Google Scholar 

  25. Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 17–34. Springer, Heidelberg (2014). doi:10.1007/978-3-319-08867-9_2. ISBN 978-3-319-08866-2

    Google Scholar 

  26. Kroening, D., Strichman, O.: Decision Procedures. Springer, Heidelberg (2008). ISBN 978-3-540-74104-6

    MATH  Google Scholar 

  27. Lahiri, S.K., Bryant, R.E.: Indexed predicate discovery for unbounded system verification. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 135–147. Springer, Heidelberg (2004). doi:10.1007/978-3-540-27813-9_11

    Chapter  Google Scholar 

  28. McMillan, K.L.: Applications of craig interpolation to model checking. In: Ciardo, G., Darondeau, P. (eds.) ICATPN 2005. LNCS, vol. 3536, pp. 15–16. Springer, Heidelberg (2005). doi:10.1007/11494744_2

    Chapter  Google Scholar 

  29. McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123–136. Springer, Heidelberg (2006). doi:10.1007/11817963_14

    Chapter  Google Scholar 

  30. McMillan, K.L.: Interpolants from Z3 proofs. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 19–27 (2011). ISBN 978-0-9835678-1-3

    Google Scholar 

  31. Monniaux, D., Alberti, F.: A simple abstraction of arrays and maps by program translation. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 217–234. Springer, Heidelberg (2015). doi:10.1007/978-3-662-48288-9_13. ISBN 978-3-662-48288-9

    Chapter  Google Scholar 

  32. Péron, M.: Contributions to the Static Analysis of Programs HandlingArrays. Theses, Université de Grenoble, September 2010. https://tel.archives-ouvertes.fr/tel-00623697

  33. Perrelle, V.: Analyse statique de programmes manipulant des tableaux. Theses, Université de Grenoble, February 2013. https://tel.archives-ouvertes.fr/tel-00973892

  34. Rival, X., Mauborgne, L.: The trace partitioning abstract domain. ACM Trans. Program. Lang. Syst., 29(5) (2007). doi:10.1145/1275497.1275501

    Google Scholar 

  35. Rümmer, P., Hojjat, H., Kuncak, V.: Disjunctive interpolants for horn-clause verification. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 347–363. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39799-8_24. ISBN 978-3-642-39798-1

    Chapter  Google Scholar 

  36. Rümmer, P., Hojjat, H., Kuncak, V.: Classifying and solving horn clauses for verification. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 1–21. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54108-7_1

    Chapter  Google Scholar 

Download references

Acknowledgments

We wish to thank the anonymous referees for their careful reading and helpful comments.

Author information

Authors and Affiliations

  1. University of Grenoble Alpes, VERIMAG, 38000, Grenoble, France

    David Monniaux

  2. CNRS, VERIMAG, 38000, Grenoble, France

    David Monniaux

  3. University of Lyon, LIP (UMR CNRS/ENS Lyon/UCB Lyon1/Inria), 69000, Lyon, France

    Laure Gonnord

Authors
  1. David Monniaux
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Laure Gonnord
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Laure Gonnord .

Editor information

Editors and Affiliations

  1. Ecole Normale Supérieure , Paris, France

    Xavier Rival

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer-Verlag GmbH Germany

About this paper

Cite this paper

Monniaux, D., Gonnord, L. (2016). Cell Morphing: From Array Programs to Array-Free Horn Clauses. In: Rival, X. (eds) Static Analysis. SAS 2016. Lecture Notes in Computer Science(), vol 9837. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-53413-7_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-53413-7_18

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-53412-0

  • Online ISBN: 978-3-662-53413-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation