Software Verification with PDR:
An Implementation of the State of the Art
Dirk Beyer
1
and Matthias Dangl
1
LMU Munich, Germany
Abstract. Property-directed reachability (PDR) is a SAT/SMT-based
reachability algorithm that incrementally constructs inductive invariants.
After it was successfully applied to hardware model checking, several
adaptations to software model checking have been proposed. We contribute a replicable and thorough comparative evaluation of the state
of the art: We (1) implemented a standalone PDR algorithm and, as
improvement, a PDR-based auxiliary-invariant generator for k -induction,
and (2) performed an experimental study on the largest publicly available
benchmark set of C verification tasks, in which we explore the effectiveness
and efficiency of software verification with PDR. The main contribution
of our work is to establish a reproducible baseline for ongoing research in
the area by providing a well-engineered reference implementation and an
experimental evaluation of the existing techniques.
Keywords: Software verification · Program analysis · Invariant generation · Property-directed reachability (PDR) · IC3 · k -Induction· VVT ·
CPAchecker
1 Introduction
Automatic software verification [24] is a broad research area with many success
stories and large impact on technology that is applied in industry [2, 14, 27].
It complements other general approaches to ensure functional correctness, like
software testing [31] and interactive software verification [3]. One large sub-area
of automatic software verification includes algorithms and approaches that are
based on SMT technology. Classic approaches like bounded model checking [10],
predicate abstraction [1, 19], and k -induction [5, 26, 32] are well understood and
evaluated; a recent survey [6] provides a uniform overview and sheds light on
the differences of the algorithms. Property-directed reachability (PDR) [12] is a
relatively recent (2011) approach that is not yet included in comparative evaluations that go beyond applying different implementations of the same or different
techniques to a set of benchmark tasks, but additionally pair such experiments
with a discussion of how the concepts can be expressed in a common formalism.
The approach was originally applied to transition systems from hardware designs,
but was also adapted to software verification [11, 12, 13, 15, 16, 25, 28, 29].
An extended version of this article is available as technical report [8].
A replication package is available on Zenodo [9].
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 3–21, 2020.
https://doi.org/10.1007/978-3-030-45190-5_1
TACAS
Evaluation
Artifact
2020
Accepted
An Implementation of the State of the Art
Dirk Beyer
1
and Matthias Dangl
1
LMU Munich, Germany
Abstract. Property-directed reachability (PDR) is a SAT/SMT-based
reachability algorithm that incrementally constructs inductive invariants.
After it was successfully applied to hardware model checking, several
adaptations to software model checking have been proposed. We contribute a replicable and thorough comparative evaluation of the state
of the art: We (1) implemented a standalone PDR algorithm and, as
improvement, a PDR-based auxiliary-invariant generator for k -induction,
and (2) performed an experimental study on the largest publicly available
benchmark set of C verification tasks, in which we explore the effectiveness
and efficiency of software verification with PDR. The main contribution
of our work is to establish a reproducible baseline for ongoing research in
the area by providing a well-engineered reference implementation and an
experimental evaluation of the existing techniques.
Keywords: Software verification · Program analysis · Invariant generation · Property-directed reachability (PDR) · IC3 · k -Induction· VVT ·
CPAchecker
1 Introduction
Automatic software verification [24] is a broad research area with many success
stories and large impact on technology that is applied in industry [2, 14, 27].
It complements other general approaches to ensure functional correctness, like
software testing [31] and interactive software verification [3]. One large sub-area
of automatic software verification includes algorithms and approaches that are
based on SMT technology. Classic approaches like bounded model checking [10],
predicate abstraction [1, 19], and k -induction [5, 26, 32] are well understood and
evaluated; a recent survey [6] provides a uniform overview and sheds light on
the differences of the algorithms. Property-directed reachability (PDR) [12] is a
relatively recent (2011) approach that is not yet included in comparative evaluations that go beyond applying different implementations of the same or different
techniques to a set of benchmark tasks, but additionally pair such experiments
with a discussion of how the concepts can be expressed in a common formalism.
The approach was originally applied to transition systems from hardware designs,
but was also adapted to software verification [11, 12, 13, 15, 16, 25, 28, 29].
An extended version of this article is available as technical report [8].
A replication package is available on Zenodo [9].
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 3–21, 2020.
https://doi.org/10.1007/978-3-030-45190-5_1
TACAS
Evaluation
Artifact
2020
Accepted