Doomed program points

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

Research output: Contribution to journalArticle

Abstract

Any programming error that can be revealed before compiling a program saves precious time for the programmer. While integrated development environments already do a good job by detecting, e.g., data-flow abnormalities, current static analysis tools suffer from false positives ("noise") or 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, regardless of which state it is started in. We use a formal verification method to identify such errors fully automatically and, most significantly, without producing noise. We report on experiments with a prototype tool.

Original languageEnglish (US)
Pages (from-to)171-199
Number of pages29
JournalFormal Methods in System Design
Volume37
Issue number2-3
DOIs
StatePublished - 2010

Keywords

  • Program falsification
  • Reliability
  • Static checking

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science
  • Hardware and Architecture

Fingerprint Dive into the research topics of 'Doomed program points'. Together they form a unique fingerprint.

  • Cite this

    Hoenicke, J., Leino, K. R. M., Podelski, A., Schäf, M., & Wies, T. (2010). Doomed program points. Formal Methods in System Design, 37(2-3), 171-199. https://doi.org/10.1007/s10703-010-0102-0