It's doomed; We can prove it

Jochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, Martin Schäf, Thomas Wies

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Original languageEnglish (US)
Title of host publicationFM 2009
Subtitle of host publicationFormal Methods - Second World Congress, Proceedings
Number of pages16
StatePublished - 2009
Event2nd World Congress on Formal Methods, FM 2009 - Eindhoven, Netherlands
Duration: Nov 2 2009Nov 6 2009

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5850 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other2nd World Congress on Formal Methods, FM 2009

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'It's doomed; We can prove it'. Together they form a unique fingerprint.

Cite this