``DySy: Dynamic symbolic execution for invariant inference''
by
Christoph Csallner,
Nikolai Tillmann,
and
Yannis Smaragdakis.
In Proc. 30th ACM/IEEE International Conference on Software
Engineering (ICSE), May 2008, pp. 281-290.
Abstract
Dynamically discovering likely program invariants from concrete test
executions has emerged as a highly promising software engineering
technique. Dynamic invariant inference has the advantage of succinctly
summarizing both ``expected'' program inputs and the subset of program
behaviors that is normal under those inputs. In this paper, we introduce a
technique that can drastically increase the relevance of inferred
invariants, or reduce the size of the test suite required to obtain good
invariants. Instead of falsifying invariants produced by pre-set patterns,
we determine likely program invariants by combining the concrete execution
of actual test cases with a simultaneous symbolic execution of the same
tests. The symbolic execution produces abstract conditions over program
variables that the concrete tests satisfy during their execution. In this
way, we obtain the benefits of dynamic inference tools like Daikon: the
inferred invariants correspond to the observed program behaviors. At the
same time, however, our inferred invariants are much more suited to the
program at hand than Daikon's hard-coded invariant patterns. The symbolic
invariants are literally derived from the program text itself, with
appropriate value substitutions as dictated by symbolic execution. We
implemented our technique in the DySy tool, which utilizes a powerful
symbolic execution and simplification engine. The results confirm the
benefits of our approach. In Daikon's prime example benchmark, we infer
the majority of the interesting Daikon invariants, while eliminating
invariants that a human user is likely to consider irrelevant.
@inproceedings{csallner08dysy,
author = {Christoph Csallner and Nikolai Tillmann and Yannis Smaragdakis},
title = {{DySy}: Dynamic symbolic execution for invariant inference},
booktitle = {Proc. 30th ACM/IEEE International Conference on Software
Engineering (ICSE)},
pages = {281--290},
publisher = {ACM},
month = may,
year = {2008}
}
Copyright notice:
This material is presented to ensure timely dissemination of scholarly and
technical work. Copyright and all rights therein are retained by authors or
by other copyright holders. All persons copying this information are
expected to adhere to the terms and constraints invoked by each author s
copyright. In most cases, these works may not be reposted without the
explicit permission of the copyright holder.