Block-Wise Abstract Interpretation by Combining Abstract Domains with SMT

DOI10.1007/978-3-319-52234-0_17zbMath1484.68049OpenAlexW2570631725MaRDI QIDQ2961574

Jiahong Jiang, Ji Wang, Liqian Chen, Xueguang Wu

Publication date: 21 February 2017

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

Full work available at URL: https://doi.org/10.1007/978-3-319-52234-0_17

zbMATH Keywords

sparsityabstract interpretationSMTabstract domainsblock encoding

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Uses Software

• Apron
• SYMBA
• UFO
• PAGAI
• BOXES
• vZ
• CIL

Cites Work

• Unnamed Item
• Why does Astrée scale up?
• The octagon abstract domain
• Donut Domains: Efficient Non-convex Domains for Abstract Interpretation
• From Under-Approximations to Over-Approximations and Back
• Linear Absolute Value Relation Analysis
• The Reduced Product of Abstract Domains and the Combination of Decision Procedures
• Interval Polyhedra: An Abstract Domain to Infer Interval Linear Relationships
• Inferring Min and Max Invariants Using Max-Plus Polyhedra
• Automatic Modular Abstractions for Template Numerical Constraints
• Boxes: A Symbolic Abstract Domain of Boxes
• Automatic modular abstractions for linear constraints
• Symbolic optimization with SMT solvers
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Block-Wise Abstract Interpretation by Combining Abstract Domains with SMT