Automatic modular abstractions for linear constraints

DOI10.1145/1480881.1480899MaRDI QIDQ5261513zbMATH OpenOpenAlexFDO

Authors 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

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)

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

Cited in

(20)

• Transfer function synthesis without quantifier elimination
• Algebraic program analysis
• Abstract interpretation of microcontroller code: intervals meet congruences
• A minimalistic look at widening operators
• Block-wise abstract interpretation by combining abstract domains with SMT
• Speeding up the constraint-based method in difference logic
• Verification, Model Checking, and Abstract Interpretation
• scientific article; zbMATH DE number 1670793 (Why is no real title available?)
• Quadtrees as an abstract domain
• Static analysis by abstract interpretation: a mathematical programming approach
• A new abstraction framework for affine transformers
• Transfer function synthesis without quantifier elimination
• Solving quantified linear arithmetic by counterexample-guided instantiation
• A modular static analysis approach to affine loop invariants detection
• Multi-prover verification of floating-point programs
• Constructing Specialized Shape Analyses for Uniform Change
• Automatic abstraction for intervals using Boolean formulae
• Static analysis by abstract interpretation of the functional correctness of matrix manipulating programs
• Improving strategies via SMT solving
• Automatic modular abstractions for template numerical constraints

Describes a project that uses

Uses Software

• ASTREE
• Octagon

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)