| |
VOLUME 6, ISSUE 3, PAPER 4
|
Automatic Modular Abstractions for Template Numerical Constraints
|
©David Monniaux, CNRS / VERIMAG
|
Abstract
We propose a method for automatically generating abstract transformers for
static analysis by abstract interpretation. The method focuses on linear
constraints on programs operating on rational, real or floating-point variables
and containing linear assignments and tests. Given the specification of an
abstract domain, and a program block, our method automatically 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 techniques over linear arithmetic formulas. We also give
less general results for nonlinear constraints and nonlinear program
constructs.
|
Publication date: July 20, 2010
Full Text: PDF | PostScript
DOI: 10.2168/LMCS-6(3:4)2010
Hit Counts: 310 |
 Creative Commons | |
