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

• 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?)
• 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
• Interpolation and SAT-based model checking.
• Lazy Abstraction with Interpolants
• Lazy abstraction
• Nested interpolants
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory

Cited in

(6)

• scientific article; zbMATH DE number 7447757 (Why is no real title available?)
• Exploiting partial variable assignment in interpolation-based model checking
• On recursion-free Horn clauses and Craig interpolation
• SMT-based verification of program changes through summary repair
• Efficient modular SMT-based model checking of pointer programs
• SMT-based model checking for recursive programs

Describes a project that uses

Uses Software

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

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)