Block-wise abstract interpretation by combining abstract domains with SMT

DOI10.1007/978-3-319-52234-0_17MaRDI QIDQ2961574zbMATH OpenOpenAlexFDO

Authors Jiahong Jiang, Liqian Chen, Xueguang Wu, Ji Wang

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

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

Recommendations

• Improving strategies via SMT solving
• Automatic abstraction for bit-vectors using decision procedures
• Refining abstract interpretations
• Theories, solvers and static analysis by abstract interpretation
• Conjunctive abstract interpretation using paramodulation

Cites work

• scientific article; zbMATH DE number 2087570 (Why is no real title available?)
• Automatic modular abstractions for linear constraints
• Automatic modular abstractions for template numerical constraints
• Boxes: A Symbolic Abstract Domain of Boxes
• Donut domains: efficient non-convex domains for abstract interpretation
• From under-approximations to over-approximations and back
• Inferring Min and Max Invariants Using Max-Plus Polyhedra
• Interval Polyhedra: An Abstract Domain to Infer Interval Linear Relationships
• Linear absolute value relation analysis
• Symbolic optimization with SMT solvers
• The octagon abstract domain
• The reduced product of abstract domains and the combination of decision procedures
• Verification, Model Checking, and Abstract Interpretation
• Verification, Model Checking, and Abstract Interpretation
• Why does Astrée scale up?

Describes a project that uses

Uses Software

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

This page was built for publication: Block-wise abstract interpretation by combining abstract domains with SMT

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