Automatic modular abstractions for linear constraints

DOI10.1145/1480881.1480899zbMATH Open1315.68102OpenAlexW2140678594MaRDI QIDQ5261513FDOQ5261513

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

Recommendations

• Automatic modular abstractions for template numerical constraints
• A modular static analysis approach to affine loop invariants detection
• scientific article; zbMATH DE number 1670793
• scientific article; zbMATH DE number 2087567
• Computer Aided Verification

zbMATH Keywords

abstract interpretationlinear inequalitiesquantifier eliminationprogram transformation

Mathematics Subject Classification ID

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

Cited In (13)

• Algebraic program analysis
• Abstract interpretation of microcontroller code: intervals meet congruences
• Improving Strategies via SMT Solving
• A minimalistic look at widening operators
• Verification, Model Checking, and Abstract Interpretation
• Title not available (Why is that?)
• Block-Wise Abstract Interpretation by Combining Abstract Domains with SMT
• Multi-Prover Verification of Floating-Point Programs
• Quadtrees as an abstract domain
• Speeding up the Constraint-Based Method in Difference Logic
• Static analysis by abstract interpretation: a mathematical programming approach
• Transfer Function Synthesis without Quantifier Elimination
• Solving quantified linear arithmetic by counterexample-guided instantiation

Uses Software

• Octagon
• ASTREE

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

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