@article{533, 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.}, author = {Hoenicke, Jochen and Leino, Kari and Podelski, Andreas and Schäf, Martin and Wies, Thomas}, journal = {Formal Methods in System Design}, number = {2-3}, pages = {171 -- 199}, publisher = {Springer}, title = {{Doomed program points}}, doi = {10.1007/s10703-010-0102-0}, volume = {37}, year = {2010}, }