{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:54:13Z","timestamp":1762458853824,"version":"3.38.0"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"2-3","license":[{"start":{"date-parts":[[2010,11,24]],"date-time":"2010-11-24T00:00:00Z","timestamp":1290556800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2010,12]]},"DOI":"10.1007\/s10703-010-0102-0","type":"journal-article","created":{"date-parts":[[2010,11,23]],"date-time":"2010-11-23T13:55:37Z","timestamp":1290520537000},"page":"171-199","source":"Crossref","is-referenced-by-count":15,"title":["Doomed program points"],"prefix":"10.1007","volume":"37","author":[{"given":"Jochen","family":"Hoenicke","sequence":"first","affiliation":[]},{"given":"K. Rustan M.","family":"Leino","sequence":"additional","affiliation":[]},{"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Sch\u00e4f","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Wies","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2010,11,24]]},"reference":[{"key":"102_CR1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1251535.1251536","volume-title":"Workshop on program analysis for software tools and engineering, PASTE\u201907","author":"N Ayewah","year":"2007","unstructured":"Ayewah N, Pugh W, Morgenthaler JD, Penix J, Zhou Y (2007) Evaluating static analysis defect warnings on production software. In: Workshop on program analysis for software tools and engineering, PASTE\u201907. ACM, New York, pp 1\u20138"},{"key":"102_CR2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/11513988_8","volume-title":"Computer aided verification, CAV\u201905","author":"T Ball","year":"2005","unstructured":"Ball T, Kupferman O, Yorsh G (2005) Abstraction for falsification. In: Computer aided verification, CAV\u201905. LNCS, vol 3576. Springer, Berlin, pp 67\u201381"},{"key":"102_CR3","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1145\/1108792.1108813","volume-title":"Workshop on program analysis for software tools and engineering, PASTE\u201905","author":"M Barnett","year":"2005","unstructured":"Barnett M, Leino KRM (2005) Weakest-precondition of unstructured programs. In: Workshop on program analysis for software tools and engineering, PASTE\u201905. ACM, New York, pp 82\u201387"},{"key":"102_CR4","series-title":"LNCS","first-page":"364","volume-title":"Formal methods for components and objects: 4th international symposium, FMCO\u201905","author":"M Barnett","year":"2005","unstructured":"Barnett M, Chang B-YE, DeLine R, Jacobs B, Leino KRM (2005) Boogie: a modular reusable verifier for object-oriented programs. In: Formal methods for components and objects: 4th international symposium, FMCO\u201905. LNCS, vol 4111. Springer, Berlin, pp 364\u2013387"},{"key":"102_CR5","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"CASSIS 2004, construction and analysis of safe, secure and interoperable smart devices","author":"M Barnett","year":"2005","unstructured":"Barnett M, Leino KRM, Schulte W (2005) The Spec# programming system: an overview. In: CASSIS 2004, construction and analysis of safe, secure and interoperable smart devices. LNCS, vol 3362. Springer, Berlin, pp 49\u201369"},{"key":"102_CR6","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1007\/3-540-63166-6_28","volume-title":"Computer aided verification, CAV\u201997","author":"I Beer","year":"1997","unstructured":"Beer I, Ben-David S, Eisner C, Rodeh Y (1997) Efficient detection of vacuity in actl formulas. In: Computer aided verification, CAV\u201997. Springer, Berlin, pp 279\u2013290"},{"key":"102_CR7","doi-asserted-by":"crossref","unstructured":"Bornat R (2000) Proving pointer programs in Hoare logic","DOI":"10.1007\/10722010_8"},{"key":"102_CR8","doi-asserted-by":"crossref","unstructured":"Burstall RM (1972) Some techniques for proving correctness of programs which alter data structures. Mach Learn 7","DOI":"10.1145\/800235.807068"},{"key":"102_CR9","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"International conference on tools and algorithms for the construction and analysis of systems, TACAS\u201904","author":"EM Clarke","year":"2004","unstructured":"Clarke EM, Kroening D, Lerda F (2004) A tool for checking ANSI-C programs. In: International conference on tools and algorithms for the construction and analysis of systems, TACAS\u201904. LNCS, vol 2988. Springer, Berlin, pp 168\u2013176"},{"key":"102_CR10","unstructured":"Cohen E, Moskal M, Schulte W, Tobies S (2000) A practical verification methodology for concurrent programs. Technical report MSR-TR-2009-15, Microsoft Research"},{"issue":"4","key":"102_CR11","doi-asserted-by":"crossref","first-page":"451","DOI":"10.1145\/115372.115320","volume":"13","author":"R Cytron","year":"1991","unstructured":"Cytron R, Ferrante J, Rosen BK, Wegman MN, Zadeck FK (1991) Efficiently computing static single assignment form and the control dependence graph. ACM Trans Program Lang Syst 13(4):451\u2013490","journal-title":"ACM Trans Program Lang Syst"},{"key":"102_CR12","volume-title":"A discipline of programming","author":"EW Dijkstra","year":"1976","unstructured":"Dijkstra EW (1976) A discipline of programming. Prentice Hall, Englewood Cliffs"},{"key":"102_CR13","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/978-3-642-03359-9_2","volume-title":"Theorem proving in higher order logics, TPHOLs\u201909","author":"MD Ernie Cohen","year":"2009","unstructured":"Ernie Cohen MD, Hillebrand M, Leinenbach D, Moskal M, Santen T, Schulte W, Tobies S (2009) VCC: a practical system for verifying concurrent C. In: Theorem proving in higher order logics, TPHOLs\u201909, pp 23\u201342"},{"issue":"1","key":"102_CR14","doi-asserted-by":"crossref","first-page":"42","DOI":"10.1109\/52.976940","volume":"19","author":"D Evans","year":"2002","unstructured":"Evans D, Larochelle D (2002) Improving security using extensible lightweight static analysis. IEEE Softw 19(1):42\u201351","journal-title":"IEEE Softw"},{"key":"102_CR15","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/978-3-540-73368-3_21","volume-title":"Computer aided verification, CAV\u201907","author":"J-C Filli\u00e2tre","year":"2007","unstructured":"Filli\u00e2tre J-C, March\u00e9 C (2007) The Why\/Krakatoa\/Caduceus platform for deductive program verification. In: Computer aided verification, CAV\u201907, pp 173\u2013177"},{"key":"102_CR16","first-page":"193","volume-title":"Annual ACM symposium on the principles of programming languages, POPL\u201901","author":"C Flanagan","year":"2001","unstructured":"Flanagan C, Saxe JB (2001) Avoiding exponential explosion: generating compact verification conditions. In: Annual ACM symposium on the principles of programming languages, POPL\u201901. ACM, New York, pp 193\u2013205"},{"key":"102_CR17","first-page":"234","volume-title":"ACM conference on programming language design and implementation, PLDI\u201902","author":"C Flanagan","year":"2002","unstructured":"Flanagan C, Leino KRM, Lillibridge M, Nelson G, Saxe JB, Stata R (2002) Extended static checking for Java. In: ACM conference on programming language design and implementation, PLDI\u201902. ACM, New York, pp 234\u2013245"},{"key":"102_CR18","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1145\/1706299.1706307","volume-title":"Annual ACM symposium on the principles of programming languages, POPL\u201910","author":"P Godefroid","year":"2010","unstructured":"Godefroid P, Nori AV, Rajamani SK, Tetali S (2010) Compositional may-must program analysis: unleashing the power of alternation. In: Annual ACM symposium on the principles of programming languages, POPL\u201910. ACM, New York, pp 43\u201356"},{"key":"102_CR19","first-page":"117","volume-title":"Symposium on the foundations of software engineering, FSE\u201906","author":"BS Gulavani","year":"2006","unstructured":"Gulavani BS, Henzinger TA, Kannan Y, Nori AV, Rajamani SK (2006) Synergy: a new algorithm for property checking. In: Symposium on the foundations of software engineering, FSE\u201906. ACM, New York, pp 117\u2013127"},{"issue":"6","key":"102_CR20","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1049\/ip-sen:20010834","volume":"148","author":"IJ Hayes","year":"2001","unstructured":"Hayes IJ, Fidge CJ, Lermer K (2001) Semantic characterisation of dead control-flow paths. IEE Proc, Softw 148(6):175\u2013186","journal-title":"IEE Proc, Softw"},{"key":"102_CR21","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1007\/3-540-44829-2_17","volume-title":"Model checking software, 10th international SPIN workshop","author":"TA Henzinger","year":"2003","unstructured":"Henzinger TA, Jhala R, Majumdar R, Sutre G (2003) Software verification with BLAST. In: Model checking software, 10th international SPIN workshop. LNCS, vol 2648. Springer, Berlin, pp 235\u2013239"},{"key":"102_CR22","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1016\/j.entcs.2009.09.063","volume":"254","author":"MA Hillebrand","year":"2009","unstructured":"Hillebrand MA, Leinenbach DC (2009) Formal verification of a reader-writer lock implementation in c. Electron Notes Theor Comput Sci 254:123\u2013141","journal-title":"Electron Notes Theor Comput Sci"},{"key":"102_CR23","first-page":"338","volume-title":"International symposium on formal methods, FM\u201909","author":"J Hoenicke","year":"2009","unstructured":"Hoenicke J, Leino KRM, Podelski A, Sch\u00e4f M, Wies T (2009) It\u2019s doomed; we can prove it. In: International symposium on formal methods, FM\u201909, pp 338\u2013353"},{"key":"102_CR24","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1145\/1251535.1251537","volume-title":"Workshop on program analysis for software tools and engineering, PASTE\u201907","author":"D Hovemeyer","year":"2007","unstructured":"Hovemeyer D, Pugh W (2007) Finding more null pointer bugs, but not too many. In: Workshop on program analysis for software tools and engineering, PASTE\u201907. ACM, New York, pp 9\u201314"},{"issue":"1","key":"102_CR25","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1145\/1108768.1108798","volume":"31","author":"D Hovemeyer","year":"2006","unstructured":"Hovemeyer D, Spacco J, Pugh W (2006) Evaluating and tuning a static analysis to find null pointer bugs. Softw Eng Notes 31(1):13\u201319","journal-title":"Softw Eng Notes"},{"key":"102_CR26","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1007\/978-3-540-30124-0_15","volume-title":"Computer science logic, CSL\u201904","author":"N Immerman","year":"2004","unstructured":"Immerman N, Rabinovich A, Reps T, Sagiv M, Yorsh G (2004) The boundary between decidability and undecidability for transitive-closure logics. In: Computer science logic, CSL\u201904, pp 160\u2013174"},{"key":"102_CR27","first-page":"23","volume-title":"Specification and verification of component-based systems, SAVCBS\u201907","author":"M Janota","year":"2007","unstructured":"Janota M, Grigore R, Moskal M (2007) Reachability analysis for annotated code. In: Specification and verification of component-based systems, SAVCBS\u201907. ACM, New York, pp 23\u201330"},{"issue":"6","key":"102_CR28","doi-asserted-by":"crossref","first-page":"1031","DOI":"10.1145\/267959.269971","volume":"19","author":"J Janssen","year":"1997","unstructured":"Janssen J, Corporaal H (1997) Making graphs reducible with controlled node splitting. ACM Trans Program Lang Syst 19(6):1031\u20131052","journal-title":"ACM Trans Program Lang Syst"},{"key":"102_CR29","unstructured":"Kuncak V (2007) Modular data structure verification. PhD thesis, EECS Department, Massachusetts Institute of Technology"},{"issue":"6","key":"102_CR30","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1016\/j.ipl.2004.10.015","volume":"93","author":"KRM Leino","year":"2005","unstructured":"Leino KRM (2005) Efficient weakest preconditions. Inf Process Lett 93(6):281\u2013288","journal-title":"Inf Process Lett"},{"key":"102_CR31","unstructured":"Leino KRM This is Boogie 2. Manuscript KRML 178, June 2008. Available at http:\/\/research.microsoft.com\/~leino\/papers.html"},{"issue":"1","key":"102_CR32","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1145\/357062.357071","volume":"1","author":"T Lengauer","year":"1979","unstructured":"Lengauer T, Tarjan RE (1979) A fast algorithm for finding dominators in a flowgraph. ACM Trans Program Lang Syst 1(1):121\u2013141","journal-title":"ACM Trans Program Lang Syst"},{"issue":"2","key":"102_CR33","doi-asserted-by":"crossref","first-page":"226","DOI":"10.1145\/357073.357078","volume":"1","author":"DC Luckham","year":"1979","unstructured":"Luckham DC, Suzuki N (1979) Verification of array, record, and pointer operations in Pascal. ACM Trans Program Lang Syst 1(2):226\u2013244","journal-title":"ACM Trans Program Lang Syst"},{"key":"102_CR34","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal verification of reactive systems: safety","author":"Z Manna","year":"1995","unstructured":"Manna Z, Pnueli A (1995) Temporal verification of reactive systems: safety. Springer, Berlin"},{"issue":"4","key":"102_CR35","doi-asserted-by":"crossref","first-page":"517","DOI":"10.1145\/69558.69559","volume":"11","author":"G Nelson","year":"1989","unstructured":"Nelson G (1989) A generalization of Dijkstra\u2019s calculus. ACM Trans Program Lang Syst 11(4):517\u2013561","journal-title":"ACM Trans Program Lang Syst"},{"key":"102_CR36","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1145\/1460299.1460314","volume-title":"IRE-AIEE-ACM\u201959, Eastern","author":"RT Prosser","year":"1959","unstructured":"Prosser RT (1959) Applications of Boolean matrices to the analysis of flow diagrams. In: IRE-AIEE-ACM\u201959, Eastern. ACM, New York, pp 133\u2013138"},{"key":"102_CR37","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/978-3-540-75560-9_2","volume-title":"Proceedings of the 14th international conference on logic for programming, artificial intelligence and reasoning, LPAR\u201907","author":"M Samer","year":"2007","unstructured":"Samer M, Veith H (2007) On the notion of vacuous truth. In: Proceedings of the 14th international conference on logic for programming, artificial intelligence and reasoning, LPAR\u201907. Springer, Berlin, pp 2\u201314"},{"key":"102_CR38","first-page":"434","volume-title":"Asia pacific software engineering conference, APSEC","author":"VI Shelekhov","year":"1999","unstructured":"Shelekhov VI, Kuksenko SV (1999) On the practical static checker of semantic run-time errors. In: Asia pacific software engineering conference, APSEC, p 434"},{"key":"102_CR39","unstructured":"Technologies P (2004) PolySpace for C. Documentation"},{"key":"102_CR40","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1145\/1146238.1146255","volume-title":"International symposium on software testing and analysis, ISSTA\u201906","author":"G Yorsh","year":"2006","unstructured":"Yorsh G, Ball T, Sagiv M (2006) Testing, abstraction, theorem proving: better together! In: International symposium on software testing and analysis, ISSTA\u201906. ACM, New York, pp 145\u2013156"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-010-0102-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-010-0102-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-010-0102-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,28]],"date-time":"2025-02-28T04:38:28Z","timestamp":1740717508000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-010-0102-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,11,24]]},"references-count":40,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[2010,12]]}},"alternative-id":["102"],"URL":"https:\/\/doi.org\/10.1007\/s10703-010-0102-0","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2010,11,24]]}}}