Automatic Modular Abstractions for Template Numerical Constraints

c Modular Abstractions for Template Numerical Constraints David Monniaux May 26, 2010 We propose a method for automatically generating abstract transformstatic analysis by abstract interpretation. The method focuses on linear constraints on programs operating on rational, real or floatingpoint variables and containing linear assignments and tests. Given the ation of an abstract domain, and a program block, our method cally outputs an implementation of the corresponding abstract transformer. It is thus a form of program transformation. In addition to loop-free code, the same method also applies for obtaining least fixed points as functions of the precondition, which permits the analysis of loops and recursive functions. The motivation of our work is data-flow synchronous programming languages, used for building control-command embedded systems, but it also applies to imperative and functional programming. Our algorithms are based on quantifier elimination and symbolic manipulation tech...

• Type: Journal
• Year: 2010
• Where: CORR
• Authors: David Monniaux
• Keywords: Abstract Transformstatic Analysis, CORR 2010, Corresponding Abstract Transformer, Education, Template Numerical Constraints