nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

Combining Forward and Backward Abstract Interpretation of Horn Clauses

verfasst von : Alexey Bakhirkin, David Monniaux

Erschienen in: Static Analysis

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

Alternation of forward and backward analyses is a standard technique in abstract interpretation of programs, which is in particular useful when we wish to prove unreachability of some undesired program states. The current state-of-the-art technique for combining forward (bottom-up, in logic programming terms) and backward (top-down) abstract interpretation of Horn clauses is query-answer transformation. It transforms a system of Horn clauses, such that standard forward analysis can propagate constraints both forward, and backward from a goal. Query-answer transformation is effective, but has issues that we wish to address. For that, we introduce a new backward collecting semantics, which is suitable for alternating forward and backward abstract interpretation of Horn clauses. We show how the alternation can be used to prove unreachability of the goal and how every subsequent run of an analysis yields a refined model of the system. Experimentally, we observe that combining forward and backward analyses is important for analysing systems that encode questions about reachability in C programs. In particular, the combination that follows our new semantics improves the precision of our own abstract interpreter, including when compared to a forward analysis of a query-answer-transformed system.

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 Probabilistic Horn Clause Verification

Nächstes Kapitel Abstract Semantic Diffing of Evolving Concurrent Programs

Nur mit Berechtigung zugänglich

In this paper, we use the terms bottom-up and top-down in the meanings that they bear in logic programming and thus they correspond to forward and backward analysis respectively. In program analysis, bottom-up may mean from callees to callers or from children to parents in the AST, but this is not the meaning that we intend in this paper.

There may be a slight abuse of notation here. When writing down the set as \(\{p_1(\mathbf {c_1}),\cdots ,p_n(\mathbf {c_n})\}\), we do not assume that all \(p_i\) or all \(\mathbf {c_i}\) are distinct and that the set has exactly n elements.

Clang: a C language family frontend for LLVM. https://clang.llvm.org/. Accessed July 2017

Competition on software verification (SV-COMP). http://sv-comp.sosy-lab.org/. Accessed July 2017

Frama-C software analyzers. https://frama-c.com/. Accessed July 2017

A path focusing abstract interpreter for horn clauses. https://gitlab.com/abakhirkin/hcai. Accessed July 2017

Ahrendt, W., Beckert, B., Bubel, R., Hähnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book - From Theory to Practice. Programming and Software Engineering, vol. 10001. Springer, Heidelberg (2016). doi:10.1007/978-3-319-49812-6

Apinis, K., Seidl, H., Vojdani, V.: Side-effecting constraint systems: a swiss army knife for program analysis. In: Jhala, R., Igarashi, A. (eds.) APLAS 2012. LNCS, vol. 7705, pp. 157–172. Springer, Heidelberg (2012). doi:10.1007/978-3-642-35182-2_12 CrossRef

Bagnara, R., Hill, P.M., Zaffanella, E.: The parma polyhedra library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1–2), 3–21 (2008)MathSciNetCrossRef

Benoy, F., King, A.: Inferring argument size relationships with CLP(\(\cal{R}\)). In: Gallagher, J. (ed.) LOPSTR 1996. LNCS, vol. 1207, pp. 204–223. Springer, Heidelberg (1997). doi:10.1007/3-540-62718-9_12 CrossRef

Beyene, T.A., Popeea, C., Rybalchenko, A.: Solving existentially quantified horn clauses. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 869–882. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39799-8_61 CrossRef

10.

Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software model checking via large-block encoding. In: Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, Austin, Texas, USA, pp. 25–32. IEEE, 15–18 November 2009

11.

Bjørner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II. LNCS, vol. 9300, pp. 24–51. Springer, Cham (2015). doi:10.1007/978-3-319-23534-9_2 CrossRef

12.

Bjørner, N., de Moura, L., Wintersteiger, C.: Z3. https://github.com/Z3Prover/z3. Accessed July 2017

13.

Bourdoncle, F.: Sémantiques des langages impératifs d’ordre supérieur et interprétation abstraite. Ph.D. thesis, École polytechnique (1992)

14.

Bourdoncle, F.: Efficient chaotic iteration strategies with widenings. In: Bjørner, D., Broy, M., Pottosin, I.V. (eds.) Formal Methods in Programming and Their Applications. LNCS, pp. 128–141. Springer, Heidelberg (1993). doi:10.1007/BFb0039704 CrossRef

15.

Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) Principles of Programming Languages (POPL), pp. 238–252. ACM (1977)

16.

Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Aho, A.V., Zilles, S.N., Rosen, B.K. (eds.) Principles of Programming Languages (POPL), pp. 269–282. ACM Press (1979)

17.

Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. J. Log. Program. 13(2–3), 103–179 (1992)MathSciNetCrossRefMATH

18.

Cousot, P., Cousot, R.: Refining model checking by abstract interpretation. Autom. Softw. Eng. 6(1), 69–95 (1999)CrossRefMATH

19.

De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Program verification via iterated specialization. Sci. Comput. Program. 95, 149–175 (2014)CrossRef

20.

Gawlitza, T.M., Seidl, H.: Precise program analysis through strategy iteration and optimization. In: Nipkow, T., Grumberg, O., Hauptmann, B. (eds.) Software Safety and Security - Tools for Analysis and Verification, NATO Science for Peace and Security Series - D: Information and Communication Security, vol. 33, pp. 348–384. IOS Press (2012)

21.

Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. In: Vitek, J., Lin, H., Tip, F. (eds.) Programming Language Design and Implementation (PLDI), pp. 405–416. ACM (2012)

22.

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, Cham (2015). doi:10.1007/978-3-319-21690-4_20 CrossRef

23.

Henry, J., Monniaux, D., Moy, M.: PAGAI: a path sensitive static analyser. Electron. Notes Theor. Comput. Sci. 289, 15–25 (2012)CrossRef

24.

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 CrossRef

25.

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 CrossRef

26.

Jaffar, J., Maher, M.J.: Constraint logic programming: a survey. J. Log. Program. 19(20), 503–581 (1994)MathSciNetCrossRefMATH

27.

Jeannet, B.: Bddapron. http://pop-art.inrialpes.fr/~bjeannet/bjeannet-forge/bddapron/. Accessed July 2017

28.

Kafle, B., Gallagher, J.P.: Constraint specialisation in horn clause verification. In: Asai, K., Sagonas, K. (eds.) Partial Evaluation and Program Manipulation (PEPM), pp. 85–90. ACM (2015)

29.

Kafle, B., Gallagher, J.P.: Tree automata-based refinement with application to horn clause verification. In: D’Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 209–226. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46081-8_12

30.

Kafle, B., Gallagher, J.P., Morales, J.F.: Rahft: a tool for verifying horn clauses using abstract interpretation and finite tree automata. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 261–268. Springer, Cham (2016). doi:10.1007/978-3-319-41528-4_14

31.

Karpenkov, E.G., Monniaux, D., Wendler, P.: Program analysis with local policy iteration. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 127–146. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49122-5_6 CrossRef

32.

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, Cham (2014). doi:10.1007/978-3-319-08867-9_2

33.

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 CrossRef

34.

Marques-Silva, J., Janota, M., Belov, A.: Minimal sets over monotone predicates in boolean formulae. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 592–607. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39799-8_39 CrossRef

35.

Monniaux, D., Gonnord, L.: Using bounded model checking to focus fixpoint iterations. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 369–385. Springer, Heidelberg (2011). doi:10.1007/978-3-642-23702-7_27 CrossRef

36.

Monniaux, D., Gonnord, L.: Cell morphing: from array programs to array-free horn clauses. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 361–382. Springer, Heidelberg (2016). doi:10.1007/978-3-662-53413-7_18 CrossRef

37.

Peralta, J.C., Gallagher, J.P.: Convex hull abstractions in specialization of CLP programs. In: Leuschel, M. (ed.) LOPSTR 2002. LNCS, vol. 2664, pp. 90–108. Springer, Heidelberg (2003). doi:10.1007/3-540-45013-0_8 CrossRef

38.

Rival, X., Mauborgne, L.: The trace partitioning abstract domain. ACM Trans. Program. Lang. Syst. 29(5), 26 (2007)CrossRef

39.

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

40.

Sharygina, N., Veith, H. (eds.): CAV 2013. LNCS, vol. 8044. Springer, Heidelberg (2013)MATH

Titel: Combining Forward and Backward Abstract Interpretation of Horn Clauses
verfasst von: Alexey Bakhirkin
David Monniaux
Verlag: Springer International Publishing
Buch: Static Analysis
Print ISBN: 978-3-319-66705-8

Electronic ISBN: 978-3-319-66706-5

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-319-66706-5_2

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner