TY - JOUR AB - 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. AU - Hoenicke, Jochen AU - Leino, Kari AU - Podelski, Andreas AU - Schäf, Martin AU - Wies, Thomas ID - 533 IS - 2-3 JF - Formal Methods in System Design TI - Doomed program points VL - 37 ER -