Information Technology Reference
In-Depth Information
are infeasible. This risk is mitigated by the enumeration technique, which produces
short execution first. Moreover, whenever a constraint evaluates to the concrete value
⊥
, the current execution path is immediately aborted. This mitigates the overhead in-
curred by nondeterministic evaluation of quantified expressions: such expressions are
likely to occur inside
assume
statements, thus branches where they evaluate to false are
immediately abandoned. Additionally, Boogaloo transparently tests the satisfiability of
the current constraints
κ
at various points during an execution, and proceeds only if the
constraints are satisfiable; unlike
pick
which may enumerate multiple solutions, a sat-
isfiability check does not cause additional nondeterminism. One can still explore the
trade-off between few expensive symbolic executions and many cheap concrete execu-
tions by adding
pick
directives at arbitrary points.
Minimization.
In addition to producing short executions first, Boogaloo also uses a
minimization technique based on binary search (similar to the one in [12]) in order to
favor
small
integers for concrete values. In our experience, this significantly improves
readability: for example, a constraint “
x
is positive and divisible by 5” with minimiza-
tion produces the most natural solution
x
=5as first witness.
5
Experimental Evaluation
We evaluated Boogaloo on a choice of 15 examples from various sources
4
. Tab. 1 lists
the programs and some data about them. The bulk of the evaluation targets the
veri-
fication
of algorithms of various kinds, listed in the top part of the table. For each of
these problems, we constructed a correct version equipped with consistent but gener-
ally incomplete specifications, and a buggy one, obtained by injecting implementation
or specification errors. We ran Boogaloo on both versions, with the goal of generating
executions: passing executions for the correct programs, and failing executions expos-
ing the bug for the buggy programs. The rest of the programs, in the bottom part of
Tab. 1, are examples of
declarative
programming, which exercise Boogaloo's constraint
solving capabilities to generate outputs satisfying given properties, in the absence of im-
perative implementations. We now briefly mention the most interesting features of our
examples, and summarize the experimental results.
Verification.
The majority of the programs in the top part of Tab. 1 are slightly adapted
examples from the Boogie project repository
5
, verification competitions [10], or previous
work [6,14]; they contain features that exercise various aspects of the test-case gener-
ation process. Strong preconditions (such as an array being sorted in BinarySearch or
being a permutation in Invert) make generating valid executions challenging using stan-
dard testing enumeration techniques. Inlining (available in Boogie) scales poorly with
the recursive procedure calls of Fibonacci and QuickSort. The specifications of Binary-
Search, BubbleSort, QuickSort, and Invert use nested universal quantifiers with bound
variables mentioned in different predicates. QuickSort PI (partial implementation) is a
4
Examples are available online at
