It's doomed; We can prove it

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

doi:10.1007/978-3-642-05089-3_22

It's doomed; We can prove it

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

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference 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 language	English (US)
Title of host publication	FM 2009
Subtitle of host publication	Formal Methods - Second World Congress, Proceedings
Pages	338-353
Number of pages	16
DOIs	https://doi.org/10.1007/978-3-642-05089-3_22
State	Published - 2009
Event	2nd World Congress on Formal Methods, FM 2009 - Eindhoven, Netherlands Duration: Nov 2 2009 → Nov 6 2009

Publication series

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

Other

Other	2nd World Congress on Formal Methods, FM 2009
Country/Territory	Netherlands
City	Eindhoven
Period	11/2/09 → 11/6/09

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

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

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

It's doomed; We can prove it. / Hoenicke, Jochen; Leino, K. Rustan M.; Podelski, Andreas et al.
FM 2009: Formal Methods - Second World Congress, Proceedings. 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 proceeding › Conference 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. 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

@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",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "338--353",

booktitle = "FM 2009",

note = "2nd World Congress on Formal Methods, FM 2009 ; Conference date: 02-11-2009 Through 06-11-2009",

}

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

AN - SCOPUS:70649095126

SN - 3642050883

SN - 9783642050886

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

T2 - 2nd World Congress on Formal Methods, FM 2009

Y2 - 2 November 2009 through 6 November 2009

ER -

It's doomed; We can prove it

Abstract

Publication series

Other

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this