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)

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

Describes a project that uses

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)