Optimal Abstraction on Real-Valued Programs

abstraction on real-valued programs David Monniaux Laboratoire d’informatique de l’´Ecole normale sup´erieure 45, rue d’Ulm, 75230 Paris cedex 5, France June 30, 2007 In this paper, we show that it is possible to abstract program fragments using real variables using formulas in the theory of real closed This abstraction is compositional and modular. We first propose 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 rethat domain. This abstraction allows computing optimal fixed nside that abstract domain, without the need for a widening operator.

• Type: Conference
• Year: 2007
• Where: SAS
• Authors: David Monniaux
• Keywords: Abstraction, Formal Methods, Optimal Abstraction, Propose Abstraction, SAS 2007