Combining static and dynamic reasoning for bug detection

Download: PDF, JCrasher, Check 'n' Crash, DSD-Crasher.

``Combining static and dynamic reasoning for bug detection'' by Yannis Smaragdakis and Christoph Csallner. In Proc. International Conference on Tests And Proofs (TAP), Feb. 2007, pp. 1-16.

Abstract

Many static and dynamic analyses have been developed to improve program quality. Several of them are well known and widely used in practice. It is not entirely clear, however, how to put these analyses together to achieve their combined benefits. This paper reports on our experiences with building a sequence of increasingly more powerful combinations of static and dynamic analyses for bug finding in the tools JCrasher, Check 'n' Crash, and DSD-Crasher. We contrast the power and accuracy of the tools using the same example program as input to all three. At the same time, the paper discusses the philosophy behind all three tools. Specifically, we argue that trying to detect program errors (rather than to certify programs for correctness) is well integrated in the development process and a promising approach for both static and dynamic analyses. The emphasis on finding program errors influences many aspects of analysis tools, including the criteria used to evaluate them and the vocabulary of discourse.

Download: PDF, JCrasher, Check 'n' Crash, DSD-Crasher.

BibTeX entry: 

@inproceedings{smaragdakis07combining,
   author = {Yannis Smaragdakis and Christoph Csallner},
   title = {Combining static and dynamic reasoning for bug detection},
   booktitle = {Proc. International Conference on Tests And Proofs (TAP)},
   series = {LNCS},
   volume = {4454},
   pages = {1--16},
   publisher = {Springer},
   month = feb,
   year = {2007}
}

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.

Back to Christoph Csallner. This page was generated with bibtex2web.