Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Simulation and Invariance for Weak Consistency Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

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

verfasst von : David Monniaux, Laure Gonnord

Erschienen in: Static Analysis

Verlag: Springer Berlin Heidelberg

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel A Parametric Abstract Domain for Lattice-Valued Regular Expressions
Nächstes Kapitel Loopy: Programmable and Formally Verified Loop Transformations
Fußnoten
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
With the exception of pointers and references, which need special handling and may be internally converted to array accesses.
 
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
Z3 and Eldarica can also occasionally directly solve Horn clauses over arrays; we also compare to that.
 
5
Classically, we denote the sets using predicates: \(I_{i_0}(\mathbf {x})\) means \(\mathbf {x}\in I_{i_0}\).
 
6
https://​github.​com/​Z3Prover hash 7f6ef0b6c0813f2e9e8f993d45722c0e5b99e152; due to various problems we preferred not to use results from later versions.
 
7
https://​bitbucket.​org/​spacer/​code hash 7e1f9af01b796750d9097b331bb66b752ea0ee3c.
 
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
Some of these tools can however infer some simpler array invariants.
 
11
For instance, \(I_{loop}=loop(n,i,a)\), \(I_{end}=end(n,i,a)\).
 
12
also denoted by \(I^\sharp _\ell ((i,n),(k,a_k))\) for sake of readability.
 
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
It would still be possible to proceed by first analyzing the first loop, getting the scalar invariant https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-53413-7_18/429226_1_En_18_IEq150_HTML.gif at location https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-53413-7_18/429226_1_En_18_IEq151_HTML.gif , quantifying it universally as https://static-content.springer.com/image/chp%3A10.1007%2F978-3-662-53413-7_18/429226_1_En_18_IEq152_HTML.gif , then analyzing the second loop. Such an approach would however fail if this program was itself included in an outer loop.
 
15
The statement if tab[i]!=42 is decomposed into x:=a[i];if(x!=42).
 
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
Nontrivial in the sense that a human user operating a Floyd-Hoare proof assistant typically does not come up with them so easily.
 
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
Their approach is not implemented in Z3 (personal communication from N. Bjørner).
 
Literatur
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 CrossRefMATH
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 CrossRef
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 CrossRef
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 CrossRef
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 CrossRef
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 CrossRef
9.
Christ, J.: Interpolation Modulo Theories. Ph.D thesis, University of Freiburg (2015)
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
11.
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)
14.
15.
16.
Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: POPL, pp. 191–202 (2002)
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)CrossRef
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.
21.
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-1CrossRef
23.
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-1CrossRef
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
26.
Kroening, D., Strichman, O.: Decision Procedures. Springer, Heidelberg (2008). ISBN 978-3-540-74104-6MATH
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 CrossRef
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 CrossRef
29.
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
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-9CrossRef
32.
33.
34.
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-1CrossRef
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 CrossRef
Metadaten
Titel
Cell Morphing: From Array Programs to Array-Free Horn Clauses
verfasst von
David Monniaux
Laure Gonnord
Copyright-Jahr
2016
Verlag
Springer Berlin Heidelberg
Buch
Static Analysis

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

Electronic ISBN: 978-3-662-53413-7

Copyright-Jahr: 2016

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

Premium Partner

    Bildnachweise