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
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Buchtitelbild

2016 | OriginalPaper | Buchkapitel

Automating Abstract Interpretation

verfasst von : Thomas Reps, Aditya Thakur

Erschienen in: Verification, Model Checking, and Abstract Interpretation

Verlag: Springer Berlin Heidelberg

Einloggen

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

search-config
loading …

Abstract

Abstract interpretation has a reputation of being a kind of “black art,” and consequently difficult to work with. This paper describes a twenty-year quest by the first author to address this issue by raising the level of automation in abstract interpretation. The most recent leg of this journey is the subject of the second author’s 2014 Ph.D. dissertation. The paper discusses several different approaches to creating correct-by-construction analyzers. Our research has allowed us to establish connections between this problem and several other areas of computer science, including automated reasoning/decision procedures, concept learning, and constraint programming.

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
Nächstes Kapitel Viper: A Verification Infrastructure for Permission-Based Reasoning
Fußnoten
1
It is interesting to note that the roles of steps (i), (iii), and (iv) are close to the steps of splitting, propagation, and join, respectively, in our generalization of St\(\mathring{\text {a}}\)lmarck’s algorithm to perform symbolic abstraction [82]. See Sect. 5.
 
2
A slight modification to the bilateral algorithm can remove the requirement of having no infinite descending chains [78].
 
3
(i) The correctness theorem for \({ focus}\) [70, Lemmas 6.8 and 6.9]; (ii) the Embedding Theorem [70, Theorem 4.9]; (iii) the correctness theorem for the finite-differencing scheme for maintaining instrumentation relations [63, Theorem 5.3]; and (iv) the correctness theorem for \({ coerce}\) [70, Theorem 6.28].
 
Literatur
1.
Akers Jr, S.: On a theory of Boolean functions. J. SIAM 7(4), 487–498 (1959)MATH
2.
3.
4.
Arnold, G., Manevich, R., Sagiv, M., Shaham, R.: Combining shape analyses by intersecting abstractions. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 33–48. Springer, Heidelberg (2006)CrossRef
5.
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. SCP 72(1–2), 3–21 (2008)MathSciNet
6.
Balakrishnan, G., Reps, T.: WYSINWYX: what you see is not what you eXecute. TOPLAS 32(6), 202–213 (2010)CrossRef
7.
Ball, T., Podelski, A., Rajamani, S.K.: Boolean and cartesian abstraction for model checking C programs. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 268–283. Springer, Heidelberg (2001)CrossRef
8.
Barrett, E., King, A.: Range and set abstraction using SAT. ENTCS 267(1), 17–27 (2010)
9.
Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M., Sebastiani, R.: Software model checking via large-block encoding. In: FMCAD (2009)
10.
Beyer, D., Keremoglu, M., Wendler, P.: Predicate abstraction with adjustable-block encoding. In: FMCAD (2010)
11.
Boerger, E., Staerk, R.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)CrossRef
12.
Bogudlov, I., Lev-Ami, T., Reps, T., Sagiv, M.: Revamping TVLA: Making parametric shape analysis competitive. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 221–225. Springer, Heidelberg (2007)CrossRef
13.
Brauer, J., King, A.: Automatic abstraction for intervals using Boolean formulae. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 167–183. Springer, Heidelberg (2010)CrossRef
14.
Bush, W., Pincus, J., Sielaff, D.: A static analyzer for finding dynamic programming errors. Softw. Pract. Experience 30, 775–802 (2000)MATHCrossRef
15.
Calcagno, C., Distefano, D., O’Hearn, P.W., Yang, H.: Footprint analysis: A shape analysis that discovers preconditions. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 402–418. Springer, Heidelberg (2007)CrossRef
16.
Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI-C programs using SAT. FMSD 25(2–3), 125–127 (2004)
17.
Cousot, P.: Verification by abstract interpretation. In: Verification Theory and Practice (2003)
18.
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977)
19.
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL (1979)
20.
Cousot, P., Cousot, R., Mauborgne, L.: Theories, solvers and static analysis by abstract interpretation. J. ACM 59(6), Article No. 31 (2012)
21.
Cousot, P., Halbwachs, N.: Automatic discovery of linear constraints among variables of a program. In: POPL (1978)
22.
Cousot, P., Monerau, M.: Probabilistic abstract interpretation. In: Seidl, H. (ed.) Programming Languages and Systems. LNCS, vol. 7211, pp. 169–193. Springer, Heidelberg (2012)CrossRef
23.
Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symbolic Logic 22(3), 269–285 (1957)MATHMathSciNetCrossRef
24.
Distefano, D., O’Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 287–302. Springer, Heidelberg (2006)CrossRef
25.
Dong, G., Su, J.: Incremental and decremental evaluation of transitive closure by first-order queries. Inf. Comp. 120, 101–106 (1995)MATHMathSciNetCrossRef
26.
Elder, M., Gopan, D., Reps, T.: View-augmented abstractions. ENTCS 267(1), 43–57 (2010)
27.
Elder, M., Lim, J., Sharma, T., Andersen, T., Reps, T.: Abstract domains of affine relations. TOPLAS 36(4), 1–73 (2014)CrossRef
28.
Futamura, Y.: Partial evaluation of computation process - an approach to a compiler-compiler. Higher-Order and Symb. Comp., 12(4) (1999). Reprinted from Systems \(\cdot \) Computers \(\cdot \) Controls 2(5) (1971)
29.
Gopan, D., Reps, T.: Lookahead widening. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 452–466. Springer, Heidelberg (2006)CrossRef
30.
Gopan, D., Reps, T.: Guided static analysis. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 349–365. Springer, Heidelberg (2007)CrossRef
31.
Graf, S., Saïdi, H.: Construction of abstract state graphs with PVS. In: CAV (1997)
32.
Gulwani, S., Musuvathi, M.: Cover algorithms and their combination. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 193–207. Springer, Heidelberg (2008)CrossRef
33.
Gupta, A., Mumick, I. (eds.): Materialized Views: Techniques, Implementations, and Applications. The M.I.T. Press, Cambridge, MA (1999)
34.
Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The M.I.T. Press, Cambridge (2006)
35.
Jeannet, B., Loginov, A., Reps, T., Sagiv, M.: A relational approach to interprocedural shape analysis. TOPLAS 32(2), 5:1–5:2 (2010)CrossRef
36.
Johnson, S.: YACC: Yet another compiler-compiler. Technical Report Comp. Sci. Tech. Rep. 32, Bell Laboratories (1975)
37.
Jones, N., Gomard, C., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice-Hall International (1993)
38.
39.
Kearns, M.J., Vazirani, U.V.: An Introduction to Computational Learning Theory. MIT Press, Cambridge, MA, USA (1994)
40.
King, A., Søndergaard, H.: Automatic abstraction for congruences. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 197–213. Springer, Heidelberg (2010)CrossRef
41.
42.
Lev-Ami, T., Sagiv, M.: TVLA: A system for implementing static analyses. In: Palsberg, J. (ed.) Static Analysis. LNCS, vol. 1824, pp. 280–301. Springer, Heidelberg (2000)CrossRef
43.
Li, Y., Albarghouthi, A., Kincaid, Z., Gurfinkel, A., Chechik, M.: Symbolic optimization with smt solvers. In: POPL (2014)
44.
Lim, J., Lal, A., Reps, T.: Symbolic analysis via semantic reinterpretation. STTT 13(1), 61–87 (2011)CrossRef
45.
Lim, J., Reps, T.: TSL: A system for generating abstract interpreters and its application to machine-code analysis. In: TOPLAS, 35(1), (2013). Article 4
46.
Malmkjær, K.: Abstract Interpretation of Partial-Evaluation Algorithms. Ph.D. thesis, Dept. of Comp. and Inf. Sci., Kansas State Univ. (1993)
47.
McMillan, K.: Don’t-care computation using k-clause approximation. In: IWLS (2005)
48.
Miné, A.: The octagon abstract domain. In: WCRE (2001)
49.
Miné, A.: A few graph-based relational numerical abstract domains. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 117–132. Springer, Heidelberg (2002)CrossRef
50.
Miné, A., Breck, J., Reps, T.: An algorithm inspired by constraint solvers to infer inductive invariants in numeric programs. Submitted for publication (2015)
51.
Mitchell, T.: Machine Learning. WCB/McGraw-Hill, Boston, MA (1997)MATH
52.
Monniaux, D.: Abstract interpretation of probabilistic semantics. In: Palsberg, J. (ed.) Static Analysis. LNCS, vol. 1824, pp. 322–339. Springer, Heidelberg (2000)CrossRef
53.
Monniaux, D.: Automatic modular abstractions for template numerical constraints. LMCS 6(3), 4 (2010)MathSciNet
54.
Montanari, U.: Networks of constraints: Fundamental properties and applications to picture processing. Inf. Sci. 7(2), 95–132 (1974)MATHMathSciNetCrossRef
55.
Müller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: POPL (2004)
56.
Mycroft, A., Jones, N.: A relational framework for abstract interpretation. In: Programs as Data Objects (1985)
57.
Mycroft, A., Jones, N.: Data flow analysis of applicative programs using minimal function graphs. In: POPL (1986)
58.
59.
Patnaik, S., Immerman, N.: Dyn-FO: A parallel, dynamic complexity class. JCSS 55(2), 199–209 (1997)MathSciNet
60.
Pelleau, M., Miné, A., Truchet, C., Benhamou, F.: A constraint solver based on abstract domains. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 434–454. Springer, Heidelberg (2013)CrossRef
61.
Regehr, J., Reid, A.: HOIST: A system for automatically deriving static analyzers for embedded systems. In: ASPLOS (2004)
62.
Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: POPL (1995)
63.
Reps, T., Sagiv, M., Loginov, A.: Finite differencing of logical formulas for static analysis. TOPLAS 6(32), 1–55 (2010)CrossRef
64.
Reps, T., Sagiv, M., Yorsh, G.: Symbolic implementation of the best transformer. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 252–266. Springer, Heidelberg (2004)CrossRef
65.
Reps, T., Schwoon, S., Jha, S., Melski, D.: Weighted pushdown systems and their application to interprocedural dataflow analysis. SCP 58(1–2), 206–263 (2005)MATHMathSciNet
66.
Reps, T., Thakur, A.: Through the lens of abstraction. In: HCSS (2014)
67.
Reps, T., Turetsky, E., Prabhu, P.: Newtonian program analysis via tensor product. In: POPL (2016)
68.
Reynolds, J.: Separation logic: A logic for shared mutable data structures. In: LICS (2002)
69.
Sagiv, M., Reps, T., Wilhelm, R.: Solving shape-analysis problems in languages with destructive updating. TOPLAS 20(1), 1–50 (1998)CrossRef
70.
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. TOPLAS 24(3), 217–298 (2002)CrossRef
71.
Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 25–41. Springer, Heidelberg (2005)CrossRef
72.
Scherpelz, E., Lerner, S., Chambers, C.: Automatic inference of optimizer flow functions from semantic meanings. In: PLDI (2007)
73.
74.
Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. Program Flow Analysis Theory and Applications. Prentice-Hall, Englewood Cliffs (1981)
75.
Sheeran, M., Stålmarck, G.: A tutorial on Stålmarck’s proof procedure for propositional logic. Formal Methods Syst. Des. 16(1), 23–58 (2000)CrossRef
76.
Thakur, A.: Symbolic Abstraction: Algorithms and Applications. Ph.D. thesis, Comp. Sci. Dept., Univ. of Wisconsin, Madison, WI, Aug. 2014. Technical Report (1812)
77.
Thakur, A., Breck, J., Reps, T.: Satisfiability modulo abstraction for separation logic with linked lists. In: Spin Workshop (2014)
78.
Thakur, A., Elder, M., Reps, T.: Bilateral algorithms for symbolic abstraction. In: Miné, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 111–128. Springer, Heidelberg (2012)CrossRef
79.
Thakur, A., Lal, A., Lim, J., Reps, T.: PostHat and all that: Automating abstract interpretation. ENTCS 311, 15–32 (2015)
80.
Thakur, A., Lim, J., Lal, A., Burton, A., Driscoll, E., Elder, M., Andersen, T., Reps, T.: Directed proof generation for machine code. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 288–305. Springer, Heidelberg (2010)CrossRef
81.
Thakur, A., Reps, T.: A generalization of Stålmarck’s method. In: SAS (2012)
82.
Thakur, A., Reps, T.: A method for symbolic computation of abstract operations. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 174–192. Springer, Heidelberg (2012)CrossRef
83.
84.
Yahav, E.: Verifying safety properties of concurrent Java programs using 3-valued logic. In: POPL (2001)
85.
Yorsh, G., Reps, T., Sagiv, M.: Symbolically computing most-precise abstract operations for shape analysis. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 530–545. Springer, Heidelberg (2004)CrossRef
Metadaten
Titel
Automating Abstract Interpretation
verfasst von
Thomas Reps
Aditya Thakur
Copyright-Jahr
2016
Verlag
Springer Berlin Heidelberg
Buch
Verification, Model Checking, and Abstract Interpretation

Print ISBN: 978-3-662-49121-8

Electronic ISBN: 978-3-662-49122-5

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-662-49122-5_1