Paper Info
Title
A Unifying View on SMT-Based Software Verification.
Abstract
After many years of successful development of new approaches for software verification, there is a need to consolidate the knowledge about the different abstract domains and algorithms. The goal of this paper is to provide a compact and accessible presentation of four SMT-based verification approaches in order to study them in theory and in practice. We present and compare the following different “schools of thought” of software verification: bounded model checking, -induction, predicate abstraction, and lazy abstraction with interpolants. Those approaches are well-known and successful in software verification and have in common that they are based on SMT solving as the back-end technology. We reformulate all four approaches in the unifying theoretical framework of configurable program analysis and implement them in the verification framework CPA. Based on this, we can present an evaluation that thoroughly compares the different approaches, where the core differences are expressed in configuration parameters and all other variables are kept constant (such as parser front end, SMT solver, used theory in SMT formulas). We evaluate the effectiveness and the efficiency of the approaches on a large set of verification tasks and discuss the conclusions.
Year
DOI
Venue
2018
https://doi.org/10.1007/s10817-017-9432-6
J. Autom. Reasoning
Keywords
Field
DocType
Software verification,Program analysis,Bounded model checking,k,-induction,Impact,Lazy abstraction,Predicate abstraction,SMT solving
Front and back ends,Programming language,Model checking,Predicate abstraction,Algorithm,Parsing,Program analysis,CPAchecker,Mathematics,Satisfiability modulo theories,Software verification
Journal
Volume
Issue
ISSN
60
3
0168-7433
Citations 
PageRank 
References 
6
0.41
44
Authors
3
Name
Order
Citations
PageRank
Dirk Beyer11736100.85
Matthias Dangl2604.53
Philipp Wendler325114.51