Doomed program points

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

Research output: Contribution to journalArticlepeer-review

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