Optimal abstraction on real-valued programs
作者： David Monniaux
DOI: 10.1007/978-3-540-74061-2_7
关键词:
摘要: In this paper, we show that it is possible to abstract program fragments using real variables formulas in the theory of closed fields. This abstraction compositional and modular. We first propose an exact for programs without loops. Given domain (in a wide class including intervals octagons), then how obtain optimal with respect domain. allows computing fixed points inside domain, need widening operator.
springer.com
archives-ouvertes.fr
sci-hub.st 参考文章(22)
Deepak Kapur, Automatically Generating Loop Invariants Using Quantifier Elimination. Deduction and Applications. ,(2005)
Jozef Gruska, Foundations of Computing ,(1997)
K. Etessami, Analysis of Recursive Game Graphs Using Data Flow Equations verification model checking and abstract interpretation. pp. 282- 296 ,(2004) , 10.1007/978-3-540-24622-0_23
Enric Rodríguez-Carbonell, Deepak Kapur, An Abstract Interpretation Approach for Automatic Generation of Polynomial Invariants Static Analysis. pp. 280- 295 ,(2004) , 10.1007/978-3-540-27864-1_21
Sriram Sankaranarayanan, Henny B. Sipma, Zohar Manna, Scalable Analysis of Linear Systems Using Mathematical Programming Lecture Notes in Computer Science. pp. 25- 41 ,(2005) , 10.1007/978-3-540-30579-8_2
Klaus Weihrauch, Computable Analysis: An Introduction ,(2014)
Glynn Winskel, The Formal Semantics of Programming Languages: An Introduction ,(1993)
Quantifier elimination and cylindrical algebraic decomposition Texts and monographs in symbolic computation. ,(1998) , 10.1007/978-3-7091-9459-1
Saugata Basu, Richard Pollack, Marie-Franco̧ise Roy, Algorithms in real algebraic geometry Springer. ,vol. 10, ,(2003) , 10.1007/978-3-662-05355-3
Saugata Basu, Marie-Françoise Roy, Richard Pollack, Algorithms in Real Algebraic Geometry (Algorithms and Computation in Mathematics) Springer-Verlag New York, Inc.. ,(2006)