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: Formal Methods - Second World Congress, Proceedings
Pages338-353
Number of pages16
Volume5850 LNCS
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)03029743
ISSN (Electronic)16113349

Other

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

Fingerprint

Formal Verification
User Interaction
False Positive
Fragment
Programming
Prototype
Experiment
Experiments
Class
Formal verification

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

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 (Vol. 5850 LNCS, 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

It's doomed; We can prove it. / Hoenicke, Jochen; Leino, K. Rustan M; Podelski, Andreas; Schäf, Martin; Wies, Thomas.

FM 2009: Formal Methods - Second World Congress, Proceedings. Vol. 5850 LNCS 2009. p. 338-353 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5850 LNCS).

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

Hoenicke, J, Leino, KRM, Podelski, A, Schäf, M & Wies, T 2009, It's doomed; We can prove it. in FM 2009: Formal Methods - Second World Congress, Proceedings. vol. 5850 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5850 LNCS, pp. 338-353, 2nd World Congress on Formal Methods, FM 2009, Eindhoven, Netherlands, 11/2/09. https://doi.org/10.1007/978-3-642-05089-3_22
Hoenicke J, Leino KRM, Podelski A, Schäf M, Wies T. It's doomed; We can prove it. In FM 2009: Formal Methods - Second World Congress, Proceedings. Vol. 5850 LNCS. 2009. p. 338-353. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-05089-3_22
Hoenicke, Jochen ; Leino, K. Rustan M ; Podelski, Andreas ; Schäf, Martin ; Wies, Thomas. / It's doomed; We can prove it. FM 2009: Formal Methods - Second World Congress, Proceedings. Vol. 5850 LNCS 2009. pp. 338-353 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{7e68452721ed4305b64c67e0d5151897,
title = "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.",
author = "Jochen Hoenicke and Leino, {K. Rustan M} and Andreas Podelski and Martin Sch{\"a}f and Thomas Wies",
year = "2009",
doi = "10.1007/978-3-642-05089-3_22",
language = "English (US)",
isbn = "3642050883",
volume = "5850 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "338--353",
booktitle = "FM 2009: Formal Methods - Second World Congress, Proceedings",

}

TY - GEN

T1 - It's doomed; We can prove it

AU - Hoenicke, Jochen

AU - Leino, K. Rustan M

AU - Podelski, Andreas

AU - Schäf, Martin

AU - Wies, Thomas

PY - 2009

Y1 - 2009

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=70649095126&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=70649095126&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-05089-3_22

DO - 10.1007/978-3-642-05089-3_22

M3 - Conference contribution

SN - 3642050883

SN - 9783642050886

VL - 5850 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 338

EP - 353

BT - FM 2009: Formal Methods - Second World Congress, Proceedings

ER -