A unifying view on SMT-based software verification
type: Item
instance of: scholarly article
title: A unifying view on SMT-based software verification
zbMATH Open document ID: 1426.68041
author: D. Beyer
author: Matthias Dangl
author: Philipp Wendler
published in: Journal of Automated Reasoning
publication date: 2018-03-01T00:00:00Z
Mathematics Subject Classification ID: 68N30
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 6845817
zbMATH Keywords: software verification
zbMATH Keywords: program analysis
zbMATH Keywords: bounded model checking
zbMATH Keywords: \(k\)-induction
zbMATH Keywords: Impact
zbMATH Keywords: lazy abstraction
zbMATH Keywords: predicate abstraction
zbMATH Keywords: SMT solving
describes a project that uses: ESBMC
describes a project that uses: LLBMC
describes a project that uses: SeaHorn
describes a project that uses: BLAST
describes a project that uses: CBMC
describes a project that uses: SLAM
describes a project that uses: CTIGAR
describes a project that uses: CPAchecker
describes a project that uses: UFO
describes a project that uses: SMACK
describes a project that uses: PKind
MaRDI profile type: Publication
full work available at URL: s10817-017-9432-6
OpenAlex ID: W2773676607
cites work: Q5452362
cites work: From Under-Approximations to Over-Approximations and Back
cites work: Symbolic execution and program testing
cites work: An extension of lazy abstraction with interpolation for programs with arrays
cites work: Counterexample-guided abstraction refinement for symbolic model checking
cites work: Q2769592
cites work: Invariant Synthesis for Combined Theories
cites work: Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis
cites work: Q3601408
cites work: Linear reasoning. A new form of the Herbrand-Gentzen theorem
cites work: SAT-Based Model Checking without Unrolling
cites work: Graph-Based Algorithms for Boolean Function Manipulation
cites work: Infinite-state invariant checking with IC3 and predicate abstraction
cites work: Tools and Algorithms for the Construction and Analysis of Systems
cites work: Computer Aided Verification
cites work: Synthesis of Circular Compositional Program Proofs via Abduction
cites work: Splitting via Interpolants
cites work: Goal-Directed Invariant Synthesis for Model Checking Modulo Theories
cites work: Backward Reachability of Array-based Systems by SMT solving: Termination and Invariant Synthesis
cites work: A Configurable CEGAR Framework with Interpolation-Based Refinements
cites work: Refinement of Trace Abstraction
cites work: Lazy abstraction
cites work: Generalized Property Directed Reachability
cites work: Software model checking
cites work: Q4068060
cites work: Lazy Abstraction with Interpolants
cites work: Q4417909
cites work: Q4255591
cites work: Liveness checking as safety checking for infinite state spaces
DOI: 10.1007/S10817-017-9432-6
description: scientific article; zbMATH DE number 6845817