Interpolation and SAT-based model checking revisited: adoption to software verification

DOI10.1007/S10817-024-09702-9MaRDI QIDQ7009613zbMATH OpenFDO

Authors D. Beyer, Nian-Ze Lee, Philipp Wendler

Publication date 20 March 2025

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/S10817-024-09702-9

zbMATH Keywords

interpolationmodel checkingSATSMTsoftware verificationprogram analysisCPAcheckerinterpolation-based model checking

Mathematics Subject Classification ID

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

Cites work

• A unifying view on SMT-based software verification
• Abstractions from proofs
• An extension of lazy abstraction with interpolation for programs with arrays
• Automatic analysis of DMA races using model checking and k-induction
• Combining model checking and data-flow analysis
• Computer Aided Verification
• Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis
• Counterexample-guided abstraction refinement for symbolic model checking
• Goal-directed invariant synthesis for model checking modulo theories
• Interpolation and SAT-based model checking.
• Interpolation and model checking
• Lazy Abstraction with Interpolants
• Lazy abstraction
• Linear reasoning. A new form of the Herbrand-Gentzen theorem
• Predicate abstraction for software verification
• Refinement of Trace Abstraction
• SAT-Based Model Checking without Unrolling
• Satisfiability modulo theories
• Slicing Abstractions
• Software model checking
• Software verification with PDR: an implementation of the state of the art
• The MathSAT5 SMT solver
• Tools and Algorithms for the Construction and Analysis of Systems
• Transition power abstractions for deep counterexample detection

This page was built for publication: Interpolation and SAT-based model checking revisited: adoption to software verification

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