{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T17:14:52Z","timestamp":1725902092776},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642050886"},{"type":"electronic","value":"9783642050893"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-05089-3_22","type":"book-chapter","created":{"date-parts":[[2009,11,3]],"date-time":"2009-11-03T22:31:40Z","timestamp":1257287500000},"page":"338-353","source":"Crossref","is-referenced-by-count":17,"title":["It\u2019s Doomed; We Can Prove It"],"prefix":"10.1007","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","reference":[{"key":"22_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1251535.1251536","volume-title":"Workshop on Program Analysis for Software Tools and Engineering, PASTE","author":"N. Ayewah","year":"2007","unstructured":"Ayewah, N., Pugh, W., David Morgenthaler, J., Penix, J., Zhou, Y.: Evaluating static analysis defect warnings on production software. In: Workshop on Program Analysis for Software Tools and Engineering, PASTE, pp. 1\u20138. ACM, New York (2007)"},{"key":"22_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M. Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol.\u00a04111, pp. 364\u2013387. Springer, Heidelberg (2006)"},{"key":"22_CR3","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1145\/1108792.1108813","volume-title":"Workshop on Program Analysis for Software Tools and Engineering, PASTE","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. In: Workshop on Program Analysis for Software Tools and Engineering, PASTE, pp. 82\u201387. ACM, New York (2005)"},{"key":"22_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-540-71209-1_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Chatterjee","year":"2007","unstructured":"Chatterjee, S., Lahiri, S., Qadeer, S., Rakamaric, Z.: A reachability predicate for analyzing low-level software. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 19\u201333. Springer, Heidelberg (2007)"},{"key":"22_CR6","unstructured":"Cohen, E., Moskal, M., Schulte, W., Tobies, S.: A practical verification methodology for concurrent programs. Technical Report MSR-TR-2009-15, Microsoft Research (February 2009)"},{"issue":"4","key":"22_CR7","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1145\/115372.115320","volume":"13","author":"R. Cytron","year":"1991","unstructured":"Cytron, R., Ferrante, J., Rosen, B.K., Wegman, M.N., Kenneth Zadeck, F.: Efficiently computing static single assignment form and the control dependence graph. ACM Transactions on Programming Languages and Systems, TOPLAS\u00a013(4), 451\u2013490 (1991)","journal-title":"ACM Transactions on Programming Languages and Systems, TOPLAS"},{"key":"22_CR8","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice Hall, Englewood Cliffs (1976)"},{"issue":"1","key":"22_CR9","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1109\/52.976940","volume":"19","author":"D. Evans","year":"2002","unstructured":"Evans, D., Larochelle, D.: Improving security using extensible lightweight static analysis. IEEE Software\u00a019(1), 42\u201351 (2002)","journal-title":"IEEE Software"},{"key":"22_CR10","first-page":"234","volume-title":"ACM Conference on Programming Language Design and Implementation, PLDI","author":"C. Flanagan","year":"2002","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: ACM Conference on Programming Language Design and Implementation, PLDI, pp. 234\u2013245. ACM, New York (2002)"},{"key":"22_CR11","first-page":"193","volume-title":"Annual ACM Symposium on the Principles of Programming Languages, POPL","author":"C. Flanagan","year":"2001","unstructured":"Flanagan, C., Saxe, J.B.: Avoiding exponential explosion: generating compact verification conditions. In: Annual ACM Symposium on the Principles of Programming Languages, POPL, pp. 193\u2013205. ACM, New York (2001)"},{"key":"22_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/3-540-44829-2_17","volume-title":"Model Checking Software","author":"T.A. Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 235\u2013239. Springer, Heidelberg (2003)"},{"key":"22_CR13","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1145\/1251535.1251537","volume-title":"Workshop on Program Analysis for Software Tools and Engineering, PASTE","author":"D. Hovemeyer","year":"2007","unstructured":"Hovemeyer, D., Pugh, W.: Finding more null pointer bugs, but not too many. In: Workshop on Program Analysis for Software Tools and Engineering, PASTE, pp. 9\u201314. ACM, New York (2007)"},{"issue":"1","key":"22_CR14","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1145\/1108768.1108798","volume":"31","author":"D. Hovemeyer","year":"2006","unstructured":"Hovemeyer, D., Spacco, J., Pugh, W.: Evaluating and tuning a static analysis to find null pointer bugs. ACM SIGSOFT Software Engineering Notes\u00a031(1), 13\u201319 (2006)","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"issue":"6","key":"22_CR15","doi-asserted-by":"publisher","first-page":"1031","DOI":"10.1145\/267959.269971","volume":"19","author":"J. Janssen","year":"1997","unstructured":"Janssen, J., Corporaal, H.: Making graphs reducible with controlled node splitting. ACM Transactions on Programming Languages and Systems, TOPLAS\u00a019(6), 1031\u20131052 (1997)","journal-title":"ACM Transactions on Programming Languages and Systems, TOPLAS"},{"key":"22_CR16","unstructured":"Kuncak, V.: Modular Data Structure Verification. PhD thesis, EECS Department, Massachusetts Institute of Technology (February 2007)"},{"issue":"6","key":"22_CR17","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1016\/j.ipl.2004.10.015","volume":"93","author":"K. Rustan","year":"2005","unstructured":"Rustan, K., Leino, M.: Efficient weakest preconditions. Information Processing Letters, IPL\u00a093(6), 281\u2013288 (2005)","journal-title":"Information Processing Letters, IPL"},{"key":"22_CR18","unstructured":"Rustan, K., Leino, M.: This is Boogie 2. Manuscript KRML 178 (June 2008), \n                    \n                      http:\/\/research.microsoft.com\/~leino\/papers.html"},{"issue":"2","key":"22_CR19","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1145\/357073.357078","volume":"1","author":"D.C. Luckham","year":"1979","unstructured":"Luckham, D.C., Suzuki, N.: Verification of array, record, and pointer operations in Pascal. ACM Transactions on Programming Languages and Systems, TOPLAS\u00a01(2), 226\u2013244 (1979)","journal-title":"ACM Transactions on Programming Languages and Systems, TOPLAS"},{"issue":"4","key":"22_CR20","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1145\/69558.69559","volume":"11","author":"G. Nelson","year":"1989","unstructured":"Nelson, G.: A generalization of Dijkstra\u2019s calculus. ACM Transactions on Programming Languages and Systems, TOPLAS\u00a011(4), 517\u2013561 (1989)","journal-title":"ACM Transactions on Programming Languages and Systems, TOPLAS"},{"key":"22_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-540-73770-4_3","volume-title":"Tests and Proofs","author":"P. R\u00fcmmer","year":"2007","unstructured":"R\u00fcmmer, P., Shah, M.A.: Proving programs incorrect using a sequent calculus for Java Dynamic Logic. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol.\u00a04454, pp. 41\u201360. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","FM 2009: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-05089-3_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T11:19:02Z","timestamp":1619781542000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-05089-3_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642050886","9783642050893"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-05089-3_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}