A unifying view on SMT-based software verification
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 1701764 (Why is no real title available?)
- scientific article; zbMATH DE number 5506101 (Why is no real title available?)
- scientific article; zbMATH DE number 3485178 (Why is no real title available?)
- scientific article; zbMATH DE number 1324833 (Why is no real title available?)
- scientific article; zbMATH DE number 1956569 (Why is no real title available?)
- scientific article; zbMATH DE number 5254145 (Why is no real title available?)
- A configurable CEGAR framework with interpolation-based refinements
- An extension of lazy abstraction with interpolation for programs with arrays
- Backward reachability of array-based systems by SMT solving: termination and invariant synthesis
- Computer Aided Verification
- Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis
- Counterexample-guided abstraction refinement for symbolic model checking
- From under-approximations to over-approximations and back
- Generalized property directed reachability
- Goal-directed invariant synthesis for model checking modulo theories
- Graph-Based Algorithms for Boolean Function Manipulation
- Infinite-state invariant checking with IC3 and predicate abstraction
- Interpolation and SAT-based model checking.
- Invariant Synthesis for Combined Theories
- Lazy Abstraction with Interpolants
- Lazy abstraction
- Linear reasoning. A new form of the Herbrand-Gentzen theorem
- Liveness checking as safety checking for infinite state spaces
- Refinement of Trace Abstraction
- SAT-Based Model Checking without Unrolling
- Software model checking
- Splitting via Interpolants
- Symbolic execution and program testing
- Synthesis of circular compositional program proofs via abduction
- Tools and Algorithms for the Construction and Analysis of Systems
Cited in
(10)- Efficient strategies for CEGAR-based model checking
- Parallel program analysis via range splitting
- 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
- SMT-based verification of program changes through summary repair
- The \textsc{Golem} Horn solver
- Transition power abstractions for deep counterexample detection
- Function summarization modulo theories
- From under-approximations to over-approximations and back
Describes a project that uses
Uses Software
This page was built for publication: A unifying view on SMT-based software verification
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1703012)
