An Abstract Domain Extending Difference-Bound Matrices with Disequality Constraints

DOI10.1007/978-3-540-69738-1_20MaRDI QIDQ5452614zbMATH OpenOpenAlexFDO

Authors Mathias Péron, Nicolas Halbwachs

Publication date 4 April 2008

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-69738-1_20

zbMATH Keywords

abstract domainsalias analysisdifference-bound matricesdisequalitiesstatic analysis

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 1738295
• Relational abstract domain of weighted hexagons
• Compact Difference Bound Matrices
• Exploiting sparsity in difference-bound matrices
• The octagon abstract domain

Cites work

• A canonical form for generalized linear constraints
• Affine relationships among variables of a program
• An improved algorithm for transitive closure on acyclic digraphs
• scientific article; zbMATH DE number 1638645 (Why is no real title available?)
• scientific article; zbMATH DE number 5542185 (Why is no real title available?)
• scientific article; zbMATH DE number 3610766 (Why is no real title available?)
• scientific article; zbMATH DE number 3635493 (Why is no real title available?)
• scientific article; zbMATH DE number 1948392 (Why is no real title available?)
• scientific article; zbMATH DE number 1400094 (Why is no real title available?)
• scientific article; zbMATH DE number 1424030 (Why is no real title available?)
• scientific article; zbMATH DE number 5175527 (Why is no real title available?)
• Improving linear constraint propagation by changing constraint representation
• Model-checking in dense real-time
• Programming Languages and Systems
• Static Analysis in Disjunctive Numerical Domains

Cited in

(7)

• Exploiting sparsity in difference-bound matrices
• Donut domains: efficient non-convex domains for abstract interpretation
• scientific article; zbMATH DE number 1738295 (Why is no real title available?)
• Compact Difference Bound Matrices
• Controller synthesis for timeline-based games
• Clustered relational thread-modular abstract interpretation with local traces
• Controller synthesis for timeline-based games

Describes a project that uses

Uses Software

• Octagon

This page was built for publication: An Abstract Domain Extending Difference-Bound Matrices with Disequality Constraints

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