David Monniaux - Automatic Modular Abstractions for Template Numerical Constraints

lmcs:1015 - Logical Methods in Computer Science, July 20, 2010, Volume 6, Issue 3 - https://doi.org/10.2168/LMCS-6(3:4)2010
Automatic Modular Abstractions for Template Numerical Constraints

Authors: David Monniaux

    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.


    Volume: Volume 6, Issue 3
    Published on: July 20, 2010
    Accepted on: June 25, 2015
    Submitted on: September 21, 2009
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages,F.3.1,F.3.2,F.4.1

    Linked data

    Source : ScholeXplorer IsReferencedBy DOI 10.1007/978-3-319-63390-9_4
    • 10.1007/978-3-319-63390-9_4
    • 10.1007/978-3-319-63390-9_4
    Automated Resource Analysis with Coq Proof Objects
    Carbonneaux, Quentin ; Hoffmann, Jan ; Reps, Thomas ; Shao, Zhong ;

    16 Documents citing this article

    Share

    Consultation statistics

    This page has been seen 358 times.
    This article's PDF has been downloaded 356 times.