Automatic modular abstractions for template numerical constraints

DOI10.2168/LMCS-6(3:4)2010MaRDI QIDQ3575308zbMATH OpenFDO

Authors David Monniaux

Publication date 27 July 2010

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.2168/LMCS-6(3:4)2010

zbMATH Keywords

abstract interpretationprogram analysisquantifier elimination

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Automatic modular abstractions for linear constraints
• Verification, Model Checking, and Abstract Interpretation
• Invariant generation through strategy iteration in succinctly represented control flow graphs
• Abstract interpretation meets convex optimization
• Static Analysis of Numerical Algorithms

Cited in

(16)

• Abstract interpretation with higher-dimensional ellipsoids and conic extrapolation
• Abstract interpretation of microcontroller code: intervals meet congruences
• A modular static analysis approach to affine loop invariants detection
• View-augmented abstractions
• Abstracting numeric constraints with Boolean functions
• Block-wise abstract interpretation by combining abstract domains with SMT
• Sound bit-precise numerical domains
• Generalizing the template polyhedral domain
• Automatic abstraction for intervals using Boolean formulae
• Automatic repair of overflowing expressions with abstract interpretation
• Stratified static analysis based on variable dependencies
• Automatic modular abstractions for linear constraints
• Transfer function synthesis without quantifier elimination
• Transfer function synthesis without quantifier elimination
• Verification, Model Checking, and Abstract Interpretation
• A zonotopic framework for functional abstractions

Describes a project that uses

Uses Software

• Mathematica
• Scilab
• BLAST
• z3
• Aspic
• Octagon
• ASTREE

This page was built for publication: Automatic modular abstractions for template numerical constraints

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3575308)