Automatic modular abstractions for linear constraints

DOI10.1145/1480881.1480899zbMath1315.68102OpenAlexW2140678594MaRDI QIDQ5261513

David Monniaux

Publication date: 3 July 2015

Published in: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/1480881.1480899

zbMATH Keywords

quantifier eliminationprogram transformationlinear inequalitiesabstract interpretation

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (11)

Algebraic program analysis ⋮ A minimalistic look at widening operators ⋮ Solving quantified linear arithmetic by counterexample-guided instantiation ⋮ Block-Wise Abstract Interpretation by Combining Abstract Domains with SMT ⋮ Abstract interpretation of microcontroller code: intervals meet congruences ⋮ Improving Strategies via SMT Solving ⋮ Multi-Prover Verification of Floating-Point Programs ⋮ Transfer Function Synthesis without Quantifier Elimination ⋮ Static Analysis by Abstract Interpretation: A Mathematical Programming Approach ⋮ Quadtrees as an Abstract Domain ⋮ Speeding up the Constraint-Based Method in Difference Logic

Uses Software

• Octagon
• ASTREE

This page was built for publication: Automatic modular abstractions for linear constraints