Skip to main content
SpringerLink
Log in

Optimal Abstraction on Real-Valued Programs

  • Conference paper
Book cover Static Analysis (SAS 2007)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 4634))

Included in the following conference series:

Abstract

In this paper, we show that it is possible to abstract program fragments using real variables using formulas in the theory of real closed fields. This abstraction is compositional and modular. We first propose an exact abstraction for programs without loops. Given an abstract domain (in a wide class including intervals and octagons), we then show how to obtain an optimal abstraction of program fragments with respect to that domain. This abstraction allows computing optimal fixed points inside that abstract domain, without the need for a widening operator.

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. Basu, S., Pollack, R., Roy, M.-F.: Algorithms in real algebraic geometry. In: Algorithms and computation in mathematics, Springer, Heidelberg (2003)

    Google Scholar 

  2. Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In: Mogensen, T.Æ., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol. 2566, pp. 85–108. Springer, Heidelberg (2002)

    Google Scholar 

  3. Caviness, B.F., Johnson, J.R. (eds.): Quantifier elimination and cylindrical algebraic decomposition. Springer, Heidelberg (1998)

    MATH  Google Scholar 

  4. Clarisó, R., Cortadella, J.: The octahedron abstract domain. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, Springer, Heidelberg (2004)

    Google Scholar 

  5. Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. Journal of Logic Programming 13(2–3), 103–179 (1992), See http://www.di.ens.fr/~cousot

    Article  MATH  MathSciNet  Google Scholar 

  6. Kapur, D.: Automatically generating loop invariants using quantifier elimination. In: ACA (Applications of Computer Algebra) (2004)

    Google Scholar 

  7. Lang, S.: Algebra, 3rd edn. Addison-Wesley, Reading (1993)

    MATH  Google Scholar 

  8. Min{\’e}, A.: The octagon abstract domain. In: Simon, A., King, A., Howe, J. (eds.) WCRE, Analysis, Slicing, and Transformation, pp. 310–319. IEEE, Los Alamitos (2001)

    Google Scholar 

  9. Miné, A.: Relational abstract domains for the detection of floating-point run-time errors. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, Springer, Heidelberg (2004)

    Google Scholar 

  10. Rodríguez-Carbonell, E., Kapur, D.: Automatic Generation of Polynomial Loop Invariants: Algebraic Foundations. In: ISSAC 2004. International Symposium on Symbolic and Algebraic Computation 2004, pp. 266–273. ACM Press, New York (2004)

    Chapter  Google Scholar 

  11. Rodríguez-Carbonell, E., Kapur, D.: An abstract interpretation approach for automatic generation of polynomial invariants. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, Springer, Heidelberg (2004)

    Google Scholar 

  12. Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Non-linear loop invariant generation using gröbner bases. In: POPL, ACM, New York (2004)

    Google Scholar 

  13. 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. 21–47. Springer, Heidelberg (2005)

    Google Scholar 

  14. Turing, A.: On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, series 2 42, 230–265 (1936)

    Article  MATH  Google Scholar 

  15. Weihrauch, K.: Computable analysis: an introduction. In: Texts in Theoretical Computer Science, Springer, Heidelberg (2000)

    Google Scholar 

  16. Winskel, G.: The Formal Semantics of Programming Languages: An Introduction. In: Foundations of Computing, MIT Press, Cambridge (1993)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratoire d’informatique de l’École normale supérieure, 45, rue d’Ulm, 75230 Paris cedex 5, France

    David Monniaux

Authors
  1. David Monniaux
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Hanne Riis Nielson Gilberto Filé

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Monniaux, D. (2007). Optimal Abstraction on Real-Valued Programs. In: Nielson, H.R., Filé, G. (eds) Static Analysis. SAS 2007. Lecture Notes in Computer Science, vol 4634. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74061-2_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-74061-2_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-74060-5

  • Online ISBN: 978-3-540-74061-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation