Skip to main content
SpringerLink
Log in

Semantics for Abstract Interpretation-Based Static Analyzes of Temporal Properties

  • Conference paper
  • First Online:
Static Analysis (SAS 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2477))

Included in the following conference series:

Abstract

Analyzing programs with abstract interpretation often requires to use a combination of forward and backward analyzes. However, the forward analyzes are mostly reachability analyzes, which are often not precise enough when we want to check other temporal properties. In this paper we propose to combine transition systems with temporal properties (with backward modalities) to get “extended” transition systems. We define forward and backward semantics for these systems, and give indications for their combination. These semantics, which use set of trees, can be abstracted to make more precise forward and backward analyzes of programs. The combinations of these analyzes are expected to give better results than the current abstract analyzes.

This work was supported in part by the RTD project IST-1999-20527 DAEDALUS of the European IST FP5 program.

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. E.M. Clarke, O. Grumberg, and D.A. Peled. Model Checking. MIT press, 1999.

    Google Scholar 

  2. P. Cousot. Méthodes itératives de construction et d’approximation de point fixes d’opérateurs monotones sur un treillis, analyse sémantique des programmes. Thése és sciences mathématiques, University of Grenoble, March 1978.

    Google Scholar 

  3. P. Cousot. Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theoretical Computer Science, 277(1–2):47–103, 2002.

    Article  MATH  MathSciNet  Google Scholar 

  4. P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In Proceedings of the Second International Symposium on Programming, pages 106–130. Dunod, Paris, France, 1976.

    Google Scholar 

  5. P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 238–252, Los Angeles, California, 1977. ACM Press, New York, NY.

    Google Scholar 

  6. P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 2(4):511–547, August 1992.

    Google Scholar 

  7. P. Cousot and R. Cousot. Inductive definitions, semantics and abstract interpretation. In Conference Record of the Ninthteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 83–94, Albuquerque, New Mexico, January 1992. ACM Press, New York, NY.

    Google Scholar 

  8. P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Conference Record of the Fifth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 84–97, Tucson, Arizona, 1978. ACM Press, New York, NY.

    Google Scholar 

  9. Panagiotis Manolios and Richard J. Trefler. Safety and liveness in branching time. In Logic in Computer Science, pages 366-, 2001.

    Google Scholar 

  10. D. Massé. Combining backward and forward analyses of temporal properties. In O. Danvy and A. Filinski, editors, Proceedings of the Second Symposium PADO’2001, Programs as Data Objects, volume 2053 of Lecture Notes in Computer Sciences, pages 155–172, Århus, Denmark, 21–23 May 2001. Springer-Verlag, Berlin, Germany.

    Chapter  Google Scholar 

  11. Laurent Mauborgne. Representation of Sets of Trees for Abstract Interpretation. PhD thesis, École Polytechnique, 1999.

    Google Scholar 

  12. Laurent Mauborgne. An incremental unique representation for regular trees. Nordic Journal of Computing, 7(4):290–311, 2000.

    MATH  MathSciNet  Google Scholar 

  13. A. Miné. The octagon abstract domain. In AST 2001 in WCRE 2001, IEEE, pages 310–319. IEEE CS Press, October 2001. http://www.di.ens.fr~mine/publi/article-mine-padoII.pdf.

Download references

Author information

Authors and Affiliations

  1. LIX, École Polytechnique, Palaiseau, France

    Damien Massé

Authors
  1. Damien Massé
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science Facultad de Informática, Technical University of Madrid, Campus de Montegancedo, 28660, Boadilla del Monte, Madrid, Spain

    Manuel V. Hermenegildo  & Germán Puebla  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Massé, D. (2002). Semantics for Abstract Interpretation-Based Static Analyzes of Temporal Properties. In: Hermenegildo, M.V., Puebla, G. (eds) Static Analysis. SAS 2002. Lecture Notes in Computer Science, vol 2477. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45789-5_30

Download citation

  • DOI: https://doi.org/10.1007/3-540-45789-5_30

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-44235-6

  • Online ISBN: 978-3-540-45789-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation