From under-approximations to over-approximations and back
DOI10.1007/978-3-642-28756-5_12zbMATH Open1352.68140OpenAlexW86344006MaRDI QIDQ2894271FDOQ2894271
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
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)
Cited In (12)
- Exploiting partial variable assignment in interpolation-based model checking
- Integrating Topological Proofs with Model Checking to Instrument Iterative Design
- Block-Wise Abstract Interpretation by Combining Abstract Domains with SMT
- UFO
- Reusing predicate precision in value analysis
- Parallel program analysis via range splitting
- Learning inductive invariants by sampling from frequency distributions
- Predicate Abstraction in Program Verification: Survey and Current Trends
- Information Exchange Between Over- and Underapproximating Software Analyses
- A unifying view on SMT-based software verification
- TOrPEDO : witnessing model correctness with topological proofs
- SMT-based model checking for recursive programs
Uses Software
Recommendations
- Software Model Checking: Searching for Computations in the Abstract or the Concrete 👍 👎
- Combining Model Checking and Data-Flow Analysis 👍 👎
- EUFORIA: complete software model checking with uninterpreted functions 👍 👎
- Under-approximating loops in C programs for fast counterexample detection 👍 👎
- A unifying view on SMT-based software verification 👍 👎
This page was built for publication: From under-approximations to over-approximations and back
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2894271)
