{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:55:49Z","timestamp":1725562549574},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642150562"},{"type":"electronic","value":"9783642150579"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15057-9_11","type":"book-chapter","created":{"date-parts":[[2010,8,11]],"date-time":"2010-08-11T07:01:15Z","timestamp":1281510075000},"page":"157-168","source":"Crossref","is-referenced-by-count":2,"title":["To Goto Where No Statement Has Gone Before"],"prefix":"10.1007","author":[{"given":"Mike","family":"Barnett","sequence":"first","affiliation":[]},{"given":"K. Rustan M.","family":"Leino","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","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":"11_CR2","volume-title":"ACM SAC - OOPS","author":"M. Barnett","year":"2010","unstructured":"Barnett, M., F\u00e4hndrich, M., Logozzo, F.: Embedded contract languages. In: ACM SAC - OOPS, March 2010. ACM, New York (2010)"},{"key":"11_CR3","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1145\/1108792.1108813","volume-title":"PASTE 2005: The 6th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. In: PASTE 2005: The 6th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, pp. 82\u201387. ACM Press, New York (2005)"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"11_CR5","doi-asserted-by":"crossref","unstructured":"Chargu\u00e9raud, A.: Program verification through characteristic formulae. In: ACM SIGPLAN International Conference on Functional Programming (to appear, 2010)","DOI":"10.1145\/1863543.1863590"},{"key":"11_CR6","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.K., Qadeer, S., Rakamari\u0107, 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)"},{"issue":"7","key":"11_CR7","doi-asserted-by":"publisher","first-page":"811","DOI":"10.1002\/spe.4380250706","volume":"25","author":"C. Cifuentes","year":"1995","unstructured":"Cifuentes, C., John Gough, K.: Decompilation of binary programs. Software \u2014 Practice and Experience\u00a025(7), 811\u2013829 (1995)","journal-title":"Software \u2014 Practice and Experience"},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"issue":"3","key":"11_CR9","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D. Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. Journal of the ACM\u00a052(3), 365\u2013473 (2005)","journal-title":"Journal of the ACM"},{"key":"11_CR10","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)"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-73368-3_21","volume-title":"Computer Aided Verification","author":"J.-C. Filli\u00e2tre","year":"2007","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: The Why\/Krakatoa\/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 173\u2013177. Springer, Heidelberg (2007)"},{"key":"11_CR12","first-page":"193","volume-title":"Conference Record of the 28th Annual ACM Symposium on Principles of Programming Languages","author":"C. Flanagan","year":"2001","unstructured":"Flanagan, C., Saxe, J.B.: Avoiding exponential explosion: Generating compact verification conditions. In: Conference Record of the 28th Annual ACM Symposium on Principles of Programming Languages, January 2001, pp. 193\u2013205. ACM, New York (2001)"},{"key":"11_CR13","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/978-1-4615-5229-1_12","volume-title":"Behavioral Specifications of Businesses and Systems","author":"G.T. Leavens","year":"1999","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: JML: A notation for detailed design. In: Kilov, H., Rumpe, B., Simmonds, I. (eds.) Behavioral Specifications of Businesses and Systems, pp. 175\u2013188. Kluwer Academic Publishers, Dordrecht (1999)"},{"key":"11_CR14","unstructured":"Rustan, K., Leino, M.: This is Boogie 2. Manuscript KRML 178 (2008), \n                    \n                      http:\/\/research.microsoft.com\/~leino\/papers.html"},{"key":"11_CR15","series-title":"NATO Science for Peace and Security Series D: Information and Communication Security","first-page":"231","volume-title":"Engineering Methods and Tools for Software Safety and Security","author":"K.R.M. Leino","year":"2009","unstructured":"Leino, K.R.M.: Specification and verification of object-oriented software. In: Broy, M., Sitou, W., Hoare, T. (eds.) Engineering Methods and Tools for Software Safety and Security. NATO Science for Peace and Security Series D: Information and Communication Security, vol.\u00a022, pp. 231\u2013266. IOS Press, Amsterdam (2009) (Summer School Marktoberdorf 2008 lecture notes)"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-642-12002-2_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010","author":"K.R.M. Leino","year":"2010","unstructured":"Leino, K.R.M., R\u00fcmmer, P.: A polymorphic intermediate verification language: Design and logical encoding. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 312\u2013327. Springer, Heidelberg (2010)"},{"key":"11_CR17","series-title":"Series in Computer Science","volume-title":"Object-oriented Software Construction","author":"B. Meyer","year":"1988","unstructured":"Meyer, B.: Object-oriented Software Construction. Series in Computer Science. Prentice-Hall International, New York (1988)"},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"Myreen, M.O., Gordon, M.J.C., Slind, K.: Machine-code verification for multiple architectures - an application of decompilation into logic. In: FMCAD, pp. 1\u20138 (2008)","DOI":"10.1109\/FMCAD.2008.ECP.24"},{"issue":"4","key":"11_CR19","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\u00a011(4), 517\u2013561 (1989)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"11_CR20","unstructured":"Ranise, S., Tinelli, C.: The SMT-LIB Standard: Version 1.2. Technical report, Department of Computer Science, The University of Iowa (2006), \n                    \n                      http:\/\/www.SMT-LIB.org"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15057-9_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T12:46:06Z","timestamp":1619786766000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15057-9_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642150562","9783642150579"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15057-9_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}