Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis
From MaRDI portal
Publication:5429342
DOI10.1007/978-3-540-73368-3_51zbMATH Open1135.68466OpenAlexW1591856965MaRDI QIDQ5429342FDOQ5429342
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
Recommendations
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
- Parallel program analysis via range splitting
- Title not available (Why is that?)
- 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
Uses Software
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)