--- _id: '533' abstract: - lang: eng text: 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: - first_name: Jochen full_name: Hoenicke, Jochen last_name: Hoenicke - first_name: Kari full_name: Leino, Kari last_name: Leino - first_name: Andreas full_name: Podelski, Andreas last_name: Podelski - first_name: Martin full_name: Schäf, Martin last_name: Schäf - first_name: Thomas full_name: Wies, Thomas id: 447BFB88-F248-11E8-B48F-1D18A9856A87 last_name: Wies citation: ama: Hoenicke J, Leino K, Podelski A, Schäf M, Wies T. Doomed program points. Formal Methods in System Design. 2010;37(2-3):171-199. doi:10.1007/s10703-010-0102-0 apa: Hoenicke, J., Leino, K., Podelski, A., Schäf, M., & Wies, T. (2010). Doomed program points. Formal Methods in System Design. Springer. https://doi.org/10.1007/s10703-010-0102-0 chicago: Hoenicke, Jochen, Kari Leino, Andreas Podelski, Martin Schäf, and Thomas Wies. “Doomed Program Points.” Formal Methods in System Design. Springer, 2010. https://doi.org/10.1007/s10703-010-0102-0. ieee: J. Hoenicke, K. Leino, A. Podelski, M. Schäf, and T. Wies, “Doomed program points,” Formal Methods in System Design, vol. 37, no. 2–3. Springer, pp. 171–199, 2010. ista: Hoenicke J, Leino K, Podelski A, Schäf M, Wies T. 2010. Doomed program points. Formal Methods in System Design. 37(2–3), 171–199. mla: Hoenicke, Jochen, et al. “Doomed Program Points.” Formal Methods in System Design, vol. 37, no. 2–3, Springer, 2010, pp. 171–99, doi:10.1007/s10703-010-0102-0. short: J. Hoenicke, K. Leino, A. Podelski, M. Schäf, T. Wies, Formal Methods in System Design 37 (2010) 171–199. date_created: 2018-12-11T11:47:01Z date_published: 2010-12-01T00:00:00Z date_updated: 2021-01-12T08:01:28Z day: '01' department: - _id: ToHe doi: 10.1007/s10703-010-0102-0 intvolume: ' 37' issue: 2-3 language: - iso: eng month: '12' oa_version: None page: 171 - 199 publication: Formal Methods in System Design publication_status: published publisher: Springer publist_id: '7284' quality_controlled: '1' scopus_import: 1 status: public title: Doomed program points type: journal_article user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87 volume: 37 year: '2010' ...