Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis

DOI10.1007/978-3-540-73368-3_51MaRDI QIDQ5429342zbMATH OpenOpenAlexFDO

Authors D. Beyer, Grégory Théoduloz, Thomas A. Henzinger

Publication date 29 November 2007

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-73368-3_51

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Combining model checking and data-flow analysis
• scientific article; zbMATH DE number 1903343
• Software model checking
• Model checking: from hardware to software.
• Integration of a Software Model Checker into Isabelle

Cited in

(16)

• Efficient strategies for CEGAR-based model checking
• Verifying Heap-Manipulating Programs in an SMT Framework
• Analysis of correct synchronization of operating system components
• Dynamic reductions for model checking concurrent software
• Experience of improving the BLAST static verification tool
• Abstraction and abstraction refinement
• Tools and Algorithms for the Construction and Analysis of Systems
• scientific article; zbMATH DE number 1693427 (Why is no real title available?)
• Parallel program analysis via range splitting
• Leveraging Horn clause solving for compositional verification of PLC software
• Combining model checking and data-flow analysis
• Predicate Abstraction in Program Verification: Survey and Current Trends
• A unifying view on SMT-based software verification
• Invariants synthesis over a combined domain for automated program verification
• A configurable CEGAR framework with interpolation-based refinements
• Empirical software metrics for benchmarking of verification tools

Describes a project that uses

Uses Software

• PAG

This page was built for publication: Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis

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