From under-approximations to over-approximations and back

DOI10.1007/978-3-642-28756-5_12MaRDI QIDQ2894271zbMATH OpenOpenAlexFDO

Authors Aws Albarghouthi, Arie Gurfinkel, Marsha Chechik

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

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

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

Cited in

(14)

• Block-wise abstract interpretation by combining abstract domains with SMT
• Parallel program analysis via range splitting
• Predicate Abstraction in Program Verification: Survey and Current Trends
• Under-approximating loops in C programs for fast counterexample detection
• Learning inductive invariants by sampling from frequency distributions
• UFO
• TOrPEDO : witnessing model correctness with topological proofs
• Information Exchange Between Over- and Underapproximating Software Analyses
• SMT-based model checking for recursive programs
• Exploiting partial variable assignment in interpolation-based model checking
• EUFORIA: complete software model checking with uninterpreted functions
• A unifying view on SMT-based software verification
• Reusing predicate precision in value analysis
• Integrating topological proofs with model checking to instrument iterative design

Describes a project that uses

Uses Software

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

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)