Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis
From MaRDI portal
Publication:5429342
DOI10.1007/978-3-540-73368-3_51zbMath1135.68466OpenAlexW1591856965MaRDI QIDQ5429342
Dirk 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
Related Items (12)
Abstraction and Abstraction Refinement ⋮ Combining Model Checking and Data-Flow Analysis ⋮ Leveraging Horn clause solving for compositional verification of PLC software ⋮ Verifying Heap-Manipulating Programs in an SMT Framework ⋮ Dynamic Reductions for Model Checking Concurrent Software ⋮ A unifying view on SMT-based software verification ⋮ Efficient strategies for CEGAR-based model checking ⋮ Predicate Abstraction in Program Verification: Survey and Current Trends ⋮ Analysis of correct synchronization of operating system components ⋮ Empirical software metrics for benchmarking of verification tools ⋮ Experience of improving the BLAST static verification tool ⋮ Invariants Synthesis over a Combined Domain for Automated Program Verification
Uses Software
This page was built for publication: Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis