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 inequalitiesprogram transformationquantifier elimination

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)

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

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)