Skip to main content
SpringerLink
Log in

Abstracting Induction by Extrapolation and Interpolation

  • Conference paper
Book cover Verification, Model Checking, and Abstract Interpretation (VMCAI 2015)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8931))

Abstract

We introduce a unified view of induction performed by automatic verification tools to prove a given program specification This unification is done in the abstract interpretation framework using extrapolation (widening/dual-widening) and interpolation (narrowing, dual-narrowing, which are equivalent up to the exchange of the parameters). Dual-narrowing generalizes Craig interpolation in First Order Logic pre-ordered by implication to arbitrary abstract domains. An increasing iterative static analysis using extrapolation of successive iterates by widening followed by a decreasing iterative static analysis using interpolation of successive iterates by narrowing (both bounded by the specification) can be further improved by a increasing iterative static analysis using interpolation of iterates with the specification by dual-narrowing until reaching a fixpoint and checking whether it is inductive for the specification.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Albarghouthi, A., Li, Y., Gurfinkel, A., Chechik, M.: UFO: A framework for abstraction- and interpolation-based software verification. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 672–678. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  2. Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening operators for convex polyhedra. Sci. Comput. Program. 58(1-2), 28–56 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  3. Bagnara, R., Hill, P.M., Zaffanella, E.: Widening operators for powerset domains. STTT 9(3-4), 413–414 (2007)

    Article  Google Scholar 

  4. Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS/ETAPS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)

    Google Scholar 

  5. Böhme, S., Leino, K.R.M., Wolff, B.: HOL-Boogie — An interactive prover for the Boogie program-verifier. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 150–166. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  6. Burstall, R.M.: Program proving as hand simulation with a little induction. In: IFIP Congress, pp. 308–312 (1974)

    Google Scholar 

  7. Chakarov, A., Sankaranarayanan, S.: Expectation invariants for probabilistic program loops as fixed points. In: Müller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol. 8723, pp. 85–100. Springer, Heidelberg (2014)

    Google Scholar 

  8. Cimatti, A., Griggio, A., Sebastiani, R.: Efficient generation of Craig interpolants in satisfiability modulo theories. ACM Trans. Comput. Log. 12(1), 7 (2010)

    Article  MathSciNet  Google Scholar 

  9. Colby, C., Lee, P.: Trace-based program analysis. In: POPL, pp. 195–207. ACM (1996)

    Google Scholar 

  10. Cortesi, A., Filé, G., Giacobazzi, R., Palamidessi, C., Ranzato, F.: Complementation in abstract interpretation. ACM TOPLAS 19(1), 7–47 (1997)

    Article  Google Scholar 

  11. Cousot, P.: Méthodes itératives de construction et d’approximation de points fixes d’opérateurs monotones sur un treillis, analyse sémantique de programmes. Thèse d’État ès sciences mathématiques, Université Joseph Fourier, Grenoble, France (March 21, 1978)

    Google Scholar 

  12. Cousot, P., Cousot, R.: Static verification of dynamic type properties of variables. Research Report R.R. 25, Laboratoire IMAG, Université Joseph Fourier, Grenoble, France (November 1975)

    Google Scholar 

  13. Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proc. Secont Int. Symp. on Programming, pp. 106–130. Dunod, Paris (1976)

    Google Scholar 

  14. Cousot, P., Cousot, R.: Constructive versions of Tarski’s fixed point theorems. Pacific J. of Math. 82(1), 43–57 (1979)

    Article  MATH  MathSciNet  Google Scholar 

  15. Cousot, P., Cousot, R.: Induction principles for proving invariance properties of programs. In: Tools & Notions for Program Construction: An Advanced Course, pp. 75–119. Cambridge University Press (August 1982)

    Google Scholar 

  16. Cousot, P.: Semantic foundations of program analysis. In: Program Flow Analysis: Theory and Applications, ch. 10, pp. 303–342. Prentice-Hall (1981)

    Google Scholar 

  17. Cousot, P.: Methods and logics for proving programs. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), pp. 841–994. Elsevier, North-Holland (1990)

    Google Scholar 

  18. Cousot, P.: Verification by abstract interpretation. In: Dershowitz, N. (ed.) Verification: Theory and Practice. LNCS, vol. 2772, pp. 243–268. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  19. Cousot, P., Cousot, R.: Vérification statique de la cohérence dynamique des programmes. Rapport du contrat IRIA SESORI No 75-035, Laboratoire IMAG, Université Joseph Fourier, Grenoble, France, 125 p. (Septembr 23, 1975)

    Google Scholar 

  20. Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238–252. ACM (1977)

    Google Scholar 

  21. Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL, pp. 269–282. ACM (1979)

    Google Scholar 

  22. Cousot, P., Cousot, R.: Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In: Bruynooghe, M., Wirsing, M. (eds.) PLILP 1992. LNCS, vol. 631, pp. 269–295. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  23. Cousot, P., Cousot, R.: Galois connection based abstract interpretations for strictness analysis. In: Bjorner, D., Broy, M., Pottosin, I.V. (eds.) FMP&TA 1993. LNCS, vol. 735, pp. 98–127. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  24. Cousot, P., Cousot, R.: Formal language, grammar and set-constraint-based program analysis by abstract interpretation. In: FPCA, pp. 170–181. ACM (1995)

    Google Scholar 

  25. Cousot, P., Cousot, R.: Grammar semantics, analysis and parsing by abstract interpretation. TCS 412(44), 6135–6192 (2011)

    Article  MATH  MathSciNet  Google Scholar 

  26. Cousot, P., Cousot, R.: An abstract interpretation framework for termination. In: POPL, pp. 245–258. ACM (2012)

    Google Scholar 

  27. Cousot, P., Cousot, R.: A Galois connection calculus for abstract interpretation. In: POPL, pp. 3–4. ACM (2014)

    Google Scholar 

  28. Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Rival, X.: Why does Astrée scale up? Formal Methods in System Design 35(3), 229–264 (2009)

    Article  MATH  Google Scholar 

  29. Cousot, P., Cousot, R., Mauborgne, L.: Theories, solvers and static analysis by abstract interpretation. J. ACM 59(6), 31 (2012)

    Article  MathSciNet  Google Scholar 

  30. Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL, pp. 84–96. ACM (1978)

    Google Scholar 

  31. Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. Journal of Symbolic Logic 22(3), 269–285 (1957)

    Article  MATH  MathSciNet  Google Scholar 

  32. Dijkstra, E.W.: Heuristics for a calculational proof. Inf. Process. Lett. 53(3), 141–143 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  33. Dijkstra, E.W., Scholten, C.S.: Predicate calculus and program semantics. Texts and monographs in computer science. Springer (1990)

    Google Scholar 

  34. Dillig, I., Dillig, T., Li, B., McMillan, K.L.: Inductive invariant generation via abductive inference. In: OOPSLA, pp. 443–456. ACM (2013)

    Google Scholar 

  35. D’Silva, V., Haller, L., Kroening, D.: Abstract satisfaction. In: POPL, pp. 139–150. ACM (2014)

    Google Scholar 

  36. Esparza, J., Kiefer, S., Luttenberger, M.: Newtonian program analysis. J. ACM 57(6), 33 (2010)

    Article  MathSciNet  Google Scholar 

  37. Feferman, S.: Harmonious logic: Craig’s interpolation theorem and its descendants. Synthese 164(3), 341–357 (2008)

    Article  MATH  MathSciNet  Google Scholar 

  38. Feret, J.: Static analysis of digital filters. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 33–48. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  39. Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: PLDI, pp. 234–245. ACM (2002)

    Google Scholar 

  40. Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: PLDI 2002: Extended static checking for Java. SIGPLAN Notices 48(4S), 22–33 (2013)

    Article  Google Scholar 

  41. Floyd, R.: Assigning meaning to programs. In: Proc. Symposium in Applied Mathematics, vol. 19, pp. 19–32. Amer. Math. Soc. (1967)

    Google Scholar 

  42. Gange, G., Navas, J.A., Schachte, P., Søndergaard, H., Stuckey, P.J.: Abstract interpretation over non-lattice abstract domains. In: Logozzo, F., Fähndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 6–24. Springer, Heidelberg (2013)

    Google Scholar 

  43. Graf, S., Saïdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  44. Gulavani, B.S., Chakraborty, S., Nori, A.V., Rajamani, S.K.: Automatically refining abstract interpretations. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 443–458. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  45. Halbwachs, N., Henry, J.: When the decreasing sequence fails. In: Miné, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 198–213. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  46. Halbwachs, N., Proy, Y., Roumanoff, P.: Verification of real-time systems using linear relation analysis. FMSD 11(2), 157–185 (1997)

    Google Scholar 

  47. Hoare, C.A.R.: An axiomatic basis for computer programming. C. ACM 12(10), 576–580 (1969)

    Article  MATH  Google Scholar 

  48. Hoder, K., Kovács, L., Voronkov, A.: Playing in the grey area of proofs. In: POPL, pp. 259–272. ACM (2012)

    Google Scholar 

  49. Huang, G.: Constructing Craig interpolation formulas. In: Li, M., Du, D.-Z. (eds.) COCOON 1995. LNCS, vol. 959, pp. 181–190. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  50. Jeannet, B., Schrammel, P., Sankaranarayanan, S.: Abstract acceleration of general linear loops. In: POPL, pp. 529–540. ACM (2014)

    Google Scholar 

  51. Morris Jr., J.H., Wegbreit, B.: Subgoal induction. C. ACM 20(4), 209–222 (1977)

    Article  MATH  MathSciNet  Google Scholar 

  52. Lakhdar-Chaouch, L., Jeannet, B., Girault, A.: Widening with thresholds for programs with complex control graphs. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 492–502. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  53. Leino, K.R.M., Wüstholz, V.: The Dafny integrated development environment. F-IDE. EPTCS 149, 3–15 (2014)

    Article  Google Scholar 

  54. Logozzo, F., Lahiri, S.K., Fähndrich, M., Blackshear, S.: Verification modulo versions: Towards usable verification. In: PLDI, p. 32. ACM (2014)

    Google Scholar 

  55. McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  56. McMillan, K.L.: Applications of Craig interpolants in model checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 1–12. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  57. McMillan, K.L.: An interpolating theorem prover. TCS 345(1), 101–121 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  58. McMillan, K.L.: Widening and interpolation. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, p. 1. Springer, Heidelberg (2011)

    Google Scholar 

  59. Venet, A.: Abstract cofibered domains: Application to the alias analysis of untyped programs. In: Cousot, R., Schmidt, D.A. (eds.) SAS 1996. LNCS, vol. 1145, pp. 366–382. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  60. Metcalfe, G., Montagna, F., Tsinakis, C.: Amalgamation and interpolation in ordered algebras. J. of Algebra 402, 21–82 (2014)

    Article  MATH  MathSciNet  Google Scholar 

  61. Mycroft, A.: The theory and practice of transforming call-by-need into call-by-value. In: Salinesi, C., Pastor, O. (eds.) CAiSE Workshops 2011. LNCS, vol. 83, pp. 269–281. Springer, Heidelberg (2011)

    Google Scholar 

  62. Naur, P.: Proofs of algorithms by general snapshots. BIT 6, 310–316 (1966)

    Article  Google Scholar 

  63. Rival, X., Mauborgne, L.: The trace partitioning abstract domain. TOPLAS 29(5) (2007)

    Google Scholar 

  64. Scott, D.S.: Continuous lattices. In: Toposes, Algebraic Geometry and Logic. LNM, vol. 274, Springer (1972)

    Google Scholar 

  65. Scott, D., Strachey, C.: Towards a mathematical semantics for computer languages. Technical Report PRG-6, Oxford University Computer Laboratory (August 1971)

    Google Scholar 

  66. Tarski, A.: A lattice theoretical fixpoint theorem and its applications. Pacific J. of Math. 5, 285–310 (1955)

    Article  MATH  MathSciNet  Google Scholar 

  67. 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)

    Chapter  Google Scholar 

  68. Venet, A.: Abstract cofibered domains: Application to the alias analysis of untyped programs. In: Cousot, R., Schmidt, D.A. (eds.) SAS 1996. LNCS, vol. 1145, pp. 366–382. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Courant Institute of Mathematical Sciences, New York University, USA

    Patrick Cousot

Authors
  1. Patrick Cousot
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Automation, Indian Institute of Science, Bangalore, India

    Deepak D’Souza

  2. Microsoft Research India, 560001, Bangalore, India

    Akash Lal

  3. Department of Computer Science, Aalborg University, Selma Lagerlöfs Vej 300, DK-9220, Aalborg East, Denmark

    Kim Guldstrand Larsen

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Cousot, P. (2015). Abstracting Induction by Extrapolation and Interpolation. In: D’Souza, D., Lal, A., Larsen, K.G. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2015. Lecture Notes in Computer Science, vol 8931. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-46081-8_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-46081-8_2

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-46080-1

  • Online ISBN: 978-3-662-46081-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation