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

(18)

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

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)