{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:21:51Z","timestamp":1725574911473},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642180699"},{"type":"electronic","value":"9783642180705"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-18070-5_12","type":"book-chapter","created":{"date-parts":[[2011,1,15]],"date-time":"2011-01-15T09:18:02Z","timestamp":1295083082000},"page":"168-182","source":"Crossref","is-referenced-by-count":0,"title":["A Dynamic Logic for Unstructured Programs with Embedded Assertions"],"prefix":"10.1007","author":[{"given":"Mattias","family":"Ulbrich","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","first-page":"82","volume-title":"PASTE 2005","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. In: Ernst, M.D., Jensen, T.P. (eds.) PASTE 2005, pp. 82\u201387. ACM Press, New York (2005)"},{"key":"12_CR2","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Verification of Object-Oriented Software. The KeY Approach","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol.\u00a04334. Springer, Heidelberg (2007)"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/11576280_22","volume-title":"Formal Methods and Software Engineering","author":"B. Beckert","year":"2005","unstructured":"Beckert, B., Schlager, S., Schmitt, P.H.: An improved rule for while loops in deductive program verification. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol.\u00a03785, pp. 315\u2013329. Springer, Heidelberg (2005)"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-540-71067-7_15","volume-title":"Theorem Proving in Higher Order Logics","author":"S. B\u00f6hme","year":"2008","unstructured":"B\u00f6hme, S., Leino, K.R.M., Wolff, B.: HOL-boogie \u2014 an interactive prover for the boogie program-verifier. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 150\u2013166. Springer, Heidelberg (2008)"},{"key":"12_CR5","doi-asserted-by":"crossref","unstructured":"Burdy, L., Pavlova, M.: Java bytecode specification and verification. In: Liebrock, L.M. (ed.) SAC 2006. ACM, New York (2006)","DOI":"10.1145\/1141277.1141708"},{"key":"12_CR6","unstructured":"DeLine, R., Leino, K.R.M.: BoogiePL: A typed procedural language for checking object-oriented programs. Technical Report MSR-TR-2005-70, Microsoft Research, Redmond (2005)"},{"key":"12_CR7","first-page":"109","volume-title":"ISSTA 2006","author":"G. Dennis","year":"2006","unstructured":"Dennis, G., Chang, F.S.-H., Jackson, D.: Modular verification of code with SAT. In: Pollock, L.L., Pezz\u00e8, M. (eds.) ISSTA 2006, pp. 109\u2013120. ACM Press, New York (2006)"},{"key":"12_CR8","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":"12_CR9","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"D. Harel","year":"2000","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)"},{"key":"12_CR10","unstructured":"Leino, K.R.M.: This is Boogie 2, Manuscript KRML 178 (2008), \n                  \n                    http:\/\/research.microsoft.com\/~leino\/papers.html"},{"key":"12_CR11","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","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":"12_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/10930755_3","volume-title":"Theorem Proving in Higher Order Logics","author":"C.L. Quigley","year":"2003","unstructured":"Quigley, C.L.: A programming logic for java bytecode programs. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 41\u201354. Springer, Heidelberg (2003)"},{"key":"12_CR13","unstructured":"Sinz, C., Falke, S., Merz, F.: A precise memory model for low-level bounded model checking. In: Huuck, R., Klein, G., Schlich, B. (eds.) SSV 2010 (2010)"},{"key":"12_CR14","unstructured":"Stenzel, K.: Verification of Java Card Programs. PhD thesis, University of Augsburg (2005)"}],"container-title":["Lecture Notes in Computer Science","Formal Verification of Object-Oriented Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-18070-5_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,23]],"date-time":"2019-03-23T17:34:42Z","timestamp":1553362482000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-18070-5_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642180699","9783642180705"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-18070-5_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}