A unifying view on SMT-based software verification

DOI10.1007/s10817-017-9432-6zbMath1426.68041OpenAlexW2773676607MaRDI QIDQ1703012

Philipp Wendler, Matthias Dangl, Dirk Beyer

Publication date: 1 March 2018

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

Full work available at URL: https://doi.org/10.1007/s10817-017-9432-6

zbMATH Keywords

program analysissoftware verificationSMT solvingbounded model checkingpredicate abstraction\(k\)-inductionlazy abstractionImpact

Mathematics Subject Classification ID

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

Related Items (4)

Software Verification with PDR: An Implementation of the State of the Art ⋮ Loop verification with invariants and contracts ⋮ Data-driven verification of stochastic linear systems with signal temporal logic constraints ⋮ Efficient strategies for CEGAR-based model checking

Uses Software

• BLAST
• SLAM
• CPAchecker
• LLBMC
• UFO
• CBMC
• ESBMC
• SeaHorn
• PKind
• CTIGAR
• SMACK

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• An extension of lazy abstraction with interpolation for programs with arrays
• Infinite-state invariant checking with IC3 and predicate abstraction
• A Configurable CEGAR Framework with Interpolation-Based Refinements
• Generalized Property Directed Reachability
• Splitting via Interpolants
• From Under-Approximations to Over-Approximations and Back
• SAT-Based Model Checking without Unrolling
• Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis
• Linear reasoning. A new form of the Herbrand-Gentzen theorem
• Refinement of Trace Abstraction
• Counterexample-guided abstraction refinement for symbolic model checking
• Goal-Directed Invariant Synthesis for Model Checking Modulo Theories
• Graph-Based Algorithms for Boolean Function Manipulation
• Symbolic execution and program testing
• Lazy abstraction
• Software model checking
• Tools and Algorithms for the Construction and Analysis of Systems
• Synthesis of Circular Compositional Program Proofs via Abduction
• Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis
• Invariant Synthesis for Combined Theories
• Lazy Abstraction with Interpolants
• Computer Aided Verification
• Computer Aided Verification

This page was built for publication: A unifying view on SMT-based software verification