Skip to main content
SpringerLink
Log in

Abstract Interpretation of Annotated Commands

  • Conference paper
Interactive Theorem Proving (ITP 2012)

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

Included in the following conference series:

Abstract

This paper formalizes a generic abstract interpreter for a while-language, including widening and narrowing. The collecting semantics and the abstract interpreter operate on annotated commands: the program is represented as a syntax tree with the semantic information directly embedded, without auxiliary labels. The aim of the paper is simplicity of the formalization, not efficiency or precision. This is motivated by the inclusion of the material in a theorem prover based course on semantics.

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. Bertot, Y.: Structural Abstract Interpretation: A Formal Study Using COQ. In: Bove, A., Barbosa, L.S., Pardo, A., Pinto, J.S. (eds.) Language Engineering and Rigorous Software Development. LNCS, vol. 5520, pp. 153–194. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  2. Bertot, Y., Grégoire, B., Leroy, X.: A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis. In: Filliâtre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol. 3839, pp. 66–81. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  3. Cachera, D., Pichardie, D.: A Certified Denotational Abstract Interpreter. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 9–24. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  4. Cousot, P.: The calculational design of a generic abstract interpreter. In: Broy, Steinbrüggen (eds.) Calculational System Design. IOS Press (1999)

    Google Scholar 

  5. Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. 4th ACM Symp. Principles of Programming Languages, pp. 238–252 (1977)

    Google Scholar 

  6. 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 

  7. Monniaux, D.: A minimalistic look at widening operators. Higher-Order and Symbolic Computation 22, 145–154 (2009)

    Article  MathSciNet  Google Scholar 

  8. Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer (1999)

    Google Scholar 

  9. Nipkow, T.: Verified Bytecode Verifiers. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001. LNCS, vol. 2030, pp. 347–363. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  10. Nipkow, T.: Teaching Semantics with a Proof Assistant: No More LSD Trip Proofs. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 24–38. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  11. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL — A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)

    Book  MATH  Google Scholar 

  12. Pichardie, D.: Interprétation abstraite en logique intuitionniste: extraction d’analyseurs Java certifiés. Ph.D. thesis, Université Rennes 1 (2005)

    Google Scholar 

  13. Pichardie, D.: Building certified static analysers by modular construction of well-founded lattices. In: Proc. 1st International Conference on Foundations of Informatics, Computing and Software (FICS 2008). ENTCS, vol. 212, pp. 225–239 (2008)

    Google Scholar 

  14. Seo, S., Yang, H., Yi, K.: Automatic Construction of Hoare Proofs from Abstract Interpretation Results. In: Ohori, A. (ed.) APLAS 2003. LNCS, vol. 2895, pp. 230–245. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fakultät für Informatik, Technische Universität München, Germany

    Tobias Nipkow

Authors
  1. Tobias Nipkow
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Princeton University, 35 Olden Street, 08540, Princeton, NJ, USA

    Lennart Beringer

  2. School of Electrical Engineering and Computer Science, University of Ottawa, 800 King Edward Ave., K1N 6N5, Ottawa, ON, Canada

    Amy Felty

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Nipkow, T. (2012). Abstract Interpretation of Annotated Commands. In: Beringer, L., Felty, A. (eds) Interactive Theorem Proving. ITP 2012. Lecture Notes in Computer Science, vol 7406. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32347-8_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-32347-8_9

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-32346-1

  • Online ISBN: 978-3-642-32347-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation