Information Technology Reference
In-Depth Information
In most examples this does not happen—constraints are “local”—and hence concretizing
does not degrade performance. The performance difference between fully symbolic and
concretized executions for the same example is particularly conspicuous in the current
prototype implementation, which uses Z3 through a pure API and hence cannot make use
of incremental constraint solving (which would be useful to avoid solving the same con-
straints multiple times during a single symbolic execution). We speculate that incremen-
tal solving would greatly reduce the performance difference between the two concretiza-
tion strategies. Even though the current implementation has a big potential for improving
performance, the experimental results are encouraging: in particular, exposing bugs—the
primary purpose of Boogaloo—is fast, even in the presence of partial implementations.
Understanding the unexpected behavior with QuickSort, where fully symbolic execution
times out, requires further investigation.
6
Related Work
Debugging Failed Verification Attempts.
While still an incipient research area, a few
techniques have recently been proposed to help understand and debug failed attempts of
program verifiers. Sec. 2 already mentioned the Boogie Verification Debugger (BVD,
[14]); the Spec# debugger [21] implements similar functionalities which construct con-
crete counterexamples from failed Boogie runs. Two-step verification [27] compares
verification with different semantics (based on unrolling and inlining) to attribute veri-
fication failures to either inconsistent or incomplete specifications.
The fact that all these approaches are built around the output provided by a program
verifier determines their main limitations compared to Boogaloo. As we demonstrated
in Sec. 2, when verification fails because of insufficient specification, the counterexam-
ples generated by BVD or similar tools are typically uninformative or even misleading,
because they ignore the implementation even when it is correct (e.g., a loop), unless
it is comes with an accurate specification (e.g., a loop invariant). Boogaloo supports
a more incremental approach, where users can concentrate on fixing major bugs first.
Sec. 2 also discussed how inlining and unrolling (available in Boogie and automatically
used in two-step verification) ameliorate these problems, but they are also not directly
comparable to Boogaloo, since they scale poorly and require to know explicit unrolling
bounds. Of course, the finitary semantics implemented by Boogaloo comes with its
own shortcomings: if the shortest counterexamples are very long, it may be infeasible
to generate them by enumeration, whereas a static verifier's modular reasoning is insen-
sitive to the length of concrete execution paths since it is entirely symbolic; tools such
as BVD can directly work on any failed verifier attempts.
Another approach to produce readable counterexamples is restricting the input lan-
guage (e.g., [24]), trading off expressiveness for decidability. Bounded model-checking
techniques (e.g., [3]) also target standard programming languages and the verification of
properties that do not include features such as infinite mappings and unbounded quan-
tification. Boogaloo follows a different course: it supports the entire Boogie language
as used in practice, which does not restrict expressiveness a priori, but may produce
spurious counterexamples.
Te s t i n g
is the process of executing programs to make them fail. Since it is based on
execution, it is typically limited to violations of simple properties that can be efficiently
