Whale: an interpolation-based algorithm for inter-procedural verification

DOI10.1007/978-3-642-27940-9_4MaRDI QIDQ2891400zbMATH OpenOpenAlexFDO

Authors Aws Albarghouthi, Arie Gurfinkel, Marsha Chechik

Publication date 15 June 2012

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

Full work available at URL https://doi.org/10.1007/978-3-642-27940-9_4

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Propositional Interpolation and Abstract Interpretation
• Constraint solving for interpolation
• Constraint Solving for Interpolation
• Guiding Craig interpolation with domain-specific abstractions
• On recursion-free Horn clauses and Craig interpolation

Cites work

• Abstractions from proofs
• An axiomatic basis for computer programming
• Compositional may-must program analysis: unleashing the power of alternation
• Computer Aided Verification
• Efficient generation of Craig interpolants in satisfiability modulo theories
• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• scientific article; zbMATH DE number 1701764 (Why is no real title available?)
• scientific article; zbMATH DE number 1798184 (Why is no real title available?)
• scientific article; zbMATH DE number 3351180 (Why is no real title available?)
• scientific article; zbMATH DE number 3351184 (Why is no real title available?)
• Interpolation and SAT-based model checking.
• Lazy abstraction
• Lazy Abstraction with Interpolants
• Nested interpolants
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory

Cited in

(6)

• Exploiting partial variable assignment in interpolation-based model checking
• Solving constrained Horn clauses using dependence-disjoint expansions
• SMT-based model checking for recursive programs
• SMT-based verification of program changes through summary repair
• Efficient modular SMT-based model checking of pointer programs
• On recursion-free Horn clauses and Craig interpolation

Describes a project that uses

Uses Software

• YASM
• LLVM
• MathSAT
• BLAST
• SLAM
• Wolverine

This page was built for publication: Whale: an interpolation-based algorithm for inter-procedural verification

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