From Under-Approximations to Over-Approximations and Back

DOI10.1007/978-3-642-28756-5_12zbMath1352.68140OpenAlexW86344006MaRDI QIDQ2894271

Marsha Chechik, Aws Albarghouthi, Arie Gurfinkel

Publication date: 29 June 2012

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-28756-5_12

Mathematics Subject Classification ID

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

Related Items

Integrating Topological Proofs with Model Checking to Instrument Iterative Design, Reusing predicate precision in value analysis, Information Exchange Between Over- and Underapproximating Software Analyses, Block-Wise Abstract Interpretation by Combining Abstract Domains with SMT, A unifying view on SMT-based software verification, Predicate Abstraction in Program Verification: Survey and Current Trends, Learning inductive invariants by sampling from frequency distributions, SMT-based model checking for recursive programs, Exploiting partial variable assignment in interpolation-based model checking, UFO, TOrPEDO : witnessing model correctness with topological proofs

Uses Software

• BLAST
• SLAM
• z3
• LLVM
• CPAchecker
• MathSAT
• Wolverine