Information Technology Reference
In-Depth Information
evaluated at runtime and are implicit in the programming language semantics (e.g., null
dereferencing). Languages such as Eiffel [23], JML [15], and Jahob [28] incorporate a
richer language for annotations that is still executable, so as to extend the applicability
of standard testing techniques. Another line of research in testing is the combination
with static techniques, with the goal of complementing each other's strengths to search
the input state space more efficiently. In [25], we combined testing with program prov-
ing at a high level. A different array of techniques combines testing with symbolic
execution; see the recent survey [2]. Boogaloo is also based on symbolic execution, but
with a different overall goal; as future work, we will leverage other techniques from
symbolic execution to improve the enumeration of executions.
Constraint Programming
supports program definitions based on declarative
constraints, describing properties of the solution, rather than on traditional imperative
constructs. Logic programming extends functional programming languages [1]; more
recent approaches combine declarative constraints with imperative languages [20,12].
All these approaches restrict the expressiveness of the constraint language to have pre-
dictable performance and some guarantees about soundness, completeness, or both. As
briefly demonstrated in Sec. 5, Boogaloo can also be used as a Boogie-based constraint
programming language. Unless we also restrict the language of assertions, we cannot
offer strong guarantees about properties of the executions generated by Boogaloo (see
the end of Sec. 3.2 for a discussion). However, the usage as a constraint programming
language brings much flexibility to Boogaloo as a testing environment for Boogie pro-
grams, since users can achieve different trade-offs between modularity and scalability
opting for the implementation or the specification semantics.
7
Conclusions and Future Work
We presented a technique and a prototype implementation to execute programs with
complex specifications and nondeterministic constructs, written in the Boogie interme-
diate verification language.
Among the various directions for future work, let us mention: integrating domain-
specific decision procedure to reduce spurious counterexamples; improving the perfor-
mance by solving constraints incrementally and by pruning infeasible branches; more
experiments with automatically generated Boogie translations; and a user study to as-
sess the practical usability alongside Boogie.
References
1. Antoy, S., Hanus, M.: Functional logic programming. Commun. ACM 53(4), 74-85 (2010)
2. Cadar, C., Sen, K.: Symbolic execution for software testing: three decades later. Commun.
ACM 56(2), 82-90 (2013)
3. Clarke, E., Kroning, D., Sharygina, N., Yorav, K.: SATABS: SAT-based predicate abstrac-
tion for ANSI-C. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440,
pp. 570-574. Springer, Heidelberg (2005)
4. Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte,
W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: Berghofer, S.,
Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23-42.
Springer, Heidelberg (2009)
