It's Doomed; We Can Prove It

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.

• Type: Conference
• Year: 2009
• Where: FM
• Authors: Jochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, Martin Schäf, Thomas Wies
• Keywords: FM 2009, Formal Verification Method, Natural Language Processing, Programming Errors, Strong User Interaction