Software Verification with PDR: An Implementation of the State of the Art
7
applied as a fall-back engine for cases where a cheaper interpolation engine fails
to produce useful interpolants [15]. It also has been proposed to improve this
approach by tracking control-flow locations explicitly instead of symbolically [28],
thereby avoiding the problem that many iterations of the algorithm are spent
only to learn the control flow, and this idea has later been extended by several
improvements to the generalization step of PDR [29]. Another approach is to
model the program using a Boolean abstraction, which has the advantage that it
requires only few changes to the original algorithm, but the disadvantage that a
refinement procedure is necessary to handle the spurious paths introduced by the
abstraction: One such approach uses infeasible error paths (i.e., counterexampleguided abstraction refinement (CEGAR) [17]) to refine the abstraction [16],
while another (CTIGAR) uses counterexamples to induction [11]; both of these
refinement techniques use interpolation to obtain abstraction predicates; the
latter of the two techniques is used in two of the configurations we compare
in our evaluation (CPAchecker-CTIGAR and Vvt-CTIGAR [20]). A different
extension of PDR to verify infinite-state systems that does not require abstraction
refinement is property-directed k -induction [25], which increases the power of the
induction checks used in PDR by applying k-induction instead of 1-induction, and
which uses model-based generalization in addition to interpolation to reason about
potentially-infinite sets of states. Unfortunately, support for effective model-based
generalization is rare in SMT solvers
2
, making this approach impractical. In
contrast, our KIPDR algorithm presented in Sect. 3 only requires support for
interpolation, which is available in several SMT solvers.
Despite this multitude of adaptations of PDR to infinite-state systems, most
implementations in practice require their input to be encoded as transition systems.
The only available software verifiers applicable to actual C programs and implement PDR-based techniques are CPAchecker [7], SeaHorn [23], and Vvt [20].
2 Background
In this section, we briefly introduce the algorithms PDR and k -induction, which
provide the core concepts on which we base our ideas. In the following description
of PDR and k -induction, we use the following notation: given the state variables s
and s
within a state-transition system T that represents the program, predicate
I(s) denotes that s is an initial state, T (s, s
) that a transition from s to s
exists,
and P (s) that the safety property P holds for state s.
2.1 PDR
PDR maintains a list of k frames, where a frame F i is a predicate that represents
an overapproximation of all states reachable within at most 0 ≤ i ≤ k steps, and
a queue of proof obligations, which guide invariant discovery towards invariants
2 The implementation of the approach of property-directed k -induction combines two
SMT solvers, because neither of them supports all features required by the technique.
7
applied as a fall-back engine for cases where a cheaper interpolation engine fails
to produce useful interpolants [15]. It also has been proposed to improve this
approach by tracking control-flow locations explicitly instead of symbolically [28],
thereby avoiding the problem that many iterations of the algorithm are spent
only to learn the control flow, and this idea has later been extended by several
improvements to the generalization step of PDR [29]. Another approach is to
model the program using a Boolean abstraction, which has the advantage that it
requires only few changes to the original algorithm, but the disadvantage that a
refinement procedure is necessary to handle the spurious paths introduced by the
abstraction: One such approach uses infeasible error paths (i.e., counterexampleguided abstraction refinement (CEGAR) [17]) to refine the abstraction [16],
while another (CTIGAR) uses counterexamples to induction [11]; both of these
refinement techniques use interpolation to obtain abstraction predicates; the
latter of the two techniques is used in two of the configurations we compare
in our evaluation (CPAchecker-CTIGAR and Vvt-CTIGAR [20]). A different
extension of PDR to verify infinite-state systems that does not require abstraction
refinement is property-directed k -induction [25], which increases the power of the
induction checks used in PDR by applying k-induction instead of 1-induction, and
which uses model-based generalization in addition to interpolation to reason about
potentially-infinite sets of states. Unfortunately, support for effective model-based
generalization is rare in SMT solvers
2
, making this approach impractical. In
contrast, our KIPDR algorithm presented in Sect. 3 only requires support for
interpolation, which is available in several SMT solvers.
Despite this multitude of adaptations of PDR to infinite-state systems, most
implementations in practice require their input to be encoded as transition systems.
The only available software verifiers applicable to actual C programs and implement PDR-based techniques are CPAchecker [7], SeaHorn [23], and Vvt [20].
2 Background
In this section, we briefly introduce the algorithms PDR and k -induction, which
provide the core concepts on which we base our ideas. In the following description
of PDR and k -induction, we use the following notation: given the state variables s
and s
within a state-transition system T that represents the program, predicate
I(s) denotes that s is an initial state, T (s, s
) that a transition from s to s
exists,
and P (s) that the safety property P holds for state s.
2.1 PDR
PDR maintains a list of k frames, where a frame F i is a predicate that represents
an overapproximation of all states reachable within at most 0 ≤ i ≤ k steps, and
a queue of proof obligations, which guide invariant discovery towards invariants
2 The implementation of the approach of property-directed k -induction combines two
SMT solvers, because neither of them supports all features required by the technique.