Abstract
Programming errors found early are the cheapest. Tools applying to the early stage of code development exist but either they suffer from false positives (“noise”) or they require strong user interaction. We propose to avoid this deficiency by defining a new class of errors. A program fragment is doomed if its execution will inevitably fail, in whatever state it is started. We use a formal verification method to identify such errors fully automatically and, most significantly, without producing noise. We report on preliminary experiments with a prototype tool.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Ayewah, N., Pugh, W., David Morgenthaler, J., Penix, J., Zhou, Y.: Evaluating static analysis defect warnings on production software. In: Workshop on Program Analysis for Software Tools and Engineering, PASTE, pp. 1–8. ACM, New York (2007)
Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006)
Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. In: Workshop on Program Analysis for Software Tools and Engineering, PASTE, pp. 82–87. ACM, New York (2005)
Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)
Chatterjee, S., Lahiri, S., Qadeer, S., Rakamaric, Z.: A reachability predicate for analyzing low-level software. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 19–33. Springer, Heidelberg (2007)
Cohen, E., Moskal, M., Schulte, W., Tobies, S.: A practical verification methodology for concurrent programs. Technical Report MSR-TR-2009-15, Microsoft Research (February 2009)
Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Kenneth Zadeck, F.: Efficiently computing static single assignment form and the control dependence graph. ACM Transactions on Programming Languages and Systems, TOPLAS 13(4), 451–490 (1991)
Dijkstra, E.W.: A Discipline of Programming. Prentice Hall, Englewood Cliffs (1976)
Evans, D., Larochelle, D.: Improving security using extensible lightweight static analysis. IEEE Software 19(1), 42–51 (2002)
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: ACM Conference on Programming Language Design and Implementation, PLDI, pp. 234–245. ACM, New York (2002)
Flanagan, C., Saxe, J.B.: Avoiding exponential explosion: generating compact verification conditions. In: Annual ACM Symposium on the Principles of Programming Languages, POPL, pp. 193–205. ACM, New York (2001)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 235–239. Springer, Heidelberg (2003)
Hovemeyer, D., Pugh, W.: Finding more null pointer bugs, but not too many. In: Workshop on Program Analysis for Software Tools and Engineering, PASTE, pp. 9–14. ACM, New York (2007)
Hovemeyer, D., Spacco, J., Pugh, W.: Evaluating and tuning a static analysis to find null pointer bugs. ACM SIGSOFT Software Engineering Notes 31(1), 13–19 (2006)
Janssen, J., Corporaal, H.: Making graphs reducible with controlled node splitting. ACM Transactions on Programming Languages and Systems, TOPLAS 19(6), 1031–1052 (1997)
Kuncak, V.: Modular Data Structure Verification. PhD thesis, EECS Department, Massachusetts Institute of Technology (February 2007)
Rustan, K., Leino, M.: Efficient weakest preconditions. Information Processing Letters, IPL 93(6), 281–288 (2005)
Rustan, K., Leino, M.: This is Boogie 2. Manuscript KRML 178 (June 2008), http://research.microsoft.com/~leino/papers.html
Luckham, D.C., Suzuki, N.: Verification of array, record, and pointer operations in Pascal. ACM Transactions on Programming Languages and Systems, TOPLAS 1(2), 226–244 (1979)
Nelson, G.: A generalization of Dijkstra’s calculus. ACM Transactions on Programming Languages and Systems, TOPLAS 11(4), 517–561 (1989)
Rümmer, P., Shah, M.A.: Proving programs incorrect using a sequent calculus for Java Dynamic Logic. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol. 4454, pp. 41–60. Springer, Heidelberg (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hoenicke, J., Leino, K.R.M., Podelski, A., Schäf, M., Wies, T. (2009). It’s Doomed; We Can Prove It. In: Cavalcanti, A., Dams, D.R. (eds) FM 2009: Formal Methods. FM 2009. Lecture Notes in Computer Science, vol 5850. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-05089-3_22
Download citation
DOI: https://doi.org/10.1007/978-3-642-05089-3_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-05088-6
Online ISBN: 978-3-642-05089-3
eBook Packages: Computer ScienceComputer Science (R0)