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

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.

Original languageEnglish (US)
Title of host publicationFM 2009
Subtitle of host publicationFormal Methods - Second World Congress, Proceedings
Pages338-353
Number of pages16
DOIs
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

Other

Other2nd World Congress on Formal Methods, FM 2009
CountryNetherlands
CityEindhoven
Period11/2/0911/6/09

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

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

  • Cite this

    Hoenicke, J., Leino, K. R. M., Podelski, A., Schäf, M., & Wies, T. (2009). It's doomed; We can prove it. In FM 2009: Formal Methods - Second World Congress, Proceedings (pp. 338-353). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5850 LNCS). https://doi.org/10.1007/978-3-642-05089-3_22