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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Basu, S., Pollack, R., Roy, M.-F.: Algorithms in real algebraic geometry. In: Algorithms and computation in mathematics, Springer, Heidelberg (2003)
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)
Caviness, B.F., Johnson, J.R. (eds.): Quantifier elimination and cylindrical algebraic decomposition. Springer, Heidelberg (1998)
Clarisó, R., Cortadella, J.: The octahedron abstract domain. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, Springer, Heidelberg (2004)
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
Kapur, D.: Automatically generating loop invariants using quantifier elimination. In: ACA (Applications of Computer Algebra) (2004)
Lang, S.: Algebra, 3rd edn. Addison-Wesley, Reading (1993)
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)
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)
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)
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)
Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Non-linear loop invariant generation using gröbner bases. In: POPL, ACM, New York (2004)
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)
Turing, A.: On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, series 2 42, 230–265 (1936)
Weihrauch, K.: Computable analysis: an introduction. In: Texts in Theoretical Computer Science, Springer, Heidelberg (2000)
Winskel, G.: The Formal Semantics of Programming Languages: An Introduction. In: Foundations of Computing, MIT Press, Cambridge (1993)
Author information
Authors and Affiliations
Editor information
Rights 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)