{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T21:07:44Z","timestamp":1725829664520},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319243115"},{"type":"electronic","value":"9783319243122"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"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":[[2015]]},"DOI":"10.1007\/978-3-319-24312-2_21","type":"book-chapter","created":{"date-parts":[[2015,9,10]],"date-time":"2015-09-10T10:06:46Z","timestamp":1441879606000},"page":"307-322","source":"Crossref","is-referenced-by-count":6,"title":["A Dynamic Logic with Traces and Coinduction"],"prefix":"10.1007","author":[{"given":"Richard","family":"Bubel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Crystal Chang","family":"Din","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Reiner","family":"H\u00e4hnle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Keiko","family":"Nakata","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,8]]},"reference":[{"key":"21_CR1","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"Emerson, E.A., Halpern, J.Y.: \u201cSometimes\u201d and \u201cNot Never\u201d revisited: On branching versus linear time temporal logic. Journal of the ACM\u00a033, 151\u2013178 (1986)","journal-title":"Journal of the ACM"},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. Foundations of Computing. MIT Press, October 2000","DOI":"10.7551\/mitpress\/2516.001.0001"},{"key":"21_CR3","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":"21_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/3-540-36578-8_18","volume-title":"Fundamental Approaches to Software Engineering","author":"B. Beckert","year":"2003","unstructured":"Beckert, B., Mostowski, W.: A Program Logic for Handling JAVA CARD\u2019s Transaction Mechanism. In: Pezz\u00e9, M. (ed.) FASE 2003. LNCS, vol.\u00a02621, pp. 246\u2013260. Springer, Heidelberg (2003)"},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-540-30569-9_8","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"R. H\u00e4hnle","year":"2005","unstructured":"H\u00e4hnle, R., Mostowski, W.: Verification of safety properties in the presence of transactions. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 151\u2013171. Springer, Heidelberg (2005)"},{"key":"21_CR6","doi-asserted-by":"crossref","unstructured":"Schellhorn, G., Tofan, B., Ernst, G., Reif, W.: Interleaved programs and rely-guarantee reasoning with ITL. In: Combi, C., Leucker, M., Wolter, F. (eds.) 18th Intl. Symp. on Temporal Representation and Reasoning, pp. 99\u2013106. IEEE (2011)","DOI":"10.1109\/TIME.2011.12"},{"key":"21_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1007\/3-540-45744-5_51","volume-title":"Automated Reasoning","author":"B. Beckert","year":"2001","unstructured":"Beckert, B., Schlager, S.: A sequent calculus for first-order dynamic logic with trace modalities. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 626\u2013641. Springer, Heidelberg (2001)"},{"key":"21_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1007\/978-3-540-72734-7_32","volume-title":"Logical Foundations of Computer Science","author":"A. Platzer","year":"2007","unstructured":"Platzer, A.: A temporal dynamic logic for verifying hybrid system invariants. In: Artemov, S., Nerode, A. (eds.) LFCS 2007. LNCS, vol.\u00a04514, pp. 457\u2013471. Springer, Heidelberg (2007)"},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-642-38574-2_22","volume-title":"Automated Deduction \u2013 CADE-24","author":"B. Beckert","year":"2013","unstructured":"Beckert, B., Bruns, D.: Dynamic logic with trace semantics. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol.\u00a07898, pp. 315\u2013329. Springer, Heidelberg (2013)"},{"key":"21_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"488","DOI":"10.1007\/978-3-642-11957-6_26","volume-title":"Programming Languages and Systems","author":"K. Nakata","year":"2010","unstructured":"Nakata, K., Uustalu, T.: A Hoare logic for the coinductive trace-based big-step semantics of While. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 488\u2013506. Springer, Heidelberg (2010)"},{"issue":"1","key":"21_CR11","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-11(1:1)2015","volume":"11","author":"K. Nakata","year":"2015","unstructured":"Nakata, K., Uustalu, T.: A Hoare logic for the coinductive trace-based big-step semantics of While. Logical Methods in Computer Science\u00a011(1), 1\u201332 (2015)","journal-title":"Logical Methods in Computer Science"},{"key":"21_CR12","series-title":"LNCS (LNAI)","first-page":"517","volume-title":"CADE-25","author":"C. Chang Din","year":"2015","unstructured":"Chang Din, C., Bubel, R., H\u00e4hnle, R.: KeY-ABS: A deductive verification tool for the concurrent modelling language ABS. In: Felty, A., Middeldorp, A. (eds.) CADE-25. LNCS (LNAI), pp. 517\u2013526. Springer, Heidelberg (2015)"},{"key":"21_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1007\/978-3-642-25271-6_8","volume-title":"FMCO 2010","author":"E.B. Johnsen","year":"2011","unstructured":"Johnsen, E.B., H\u00e4hnle, R., Sch\u00e4fer, J., Schlatte, R., Steffen, M.: ABS: A core language for abstract behavioral specification. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol.\u00a06957, pp. 142\u2013164. Springer, Heidelberg (2011)"},{"key":"21_CR14","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/11916277_29","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"P. R\u00fcmmer","year":"2006","unstructured":"R\u00fcmmer, P.: Sequential, parallel, and quantified updates of first-order structures. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, pp. 422\u2013436. Springer, Heidelberg (2006)"},{"key":"21_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/978-3-540-31987-0_29","volume-title":"Programming Languages and Systems","author":"A. Jeffrey","year":"2005","unstructured":"Jeffrey, A., Rathke, J.: Java JR: Fully\u00a0abstract\u00a0trace\u00a0semantics for\u00a0a\u00a0core\u00a0java\u00a0language. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 423\u2013438. Springer, Heidelberg (2005)"},{"key":"21_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-540-79124-9_11","volume-title":"Tests and Proofs","author":"H. Velroyen","year":"2008","unstructured":"Velroyen, H., R\u00fcmmer, P.: Non-termination checking for imperative programs. In: Beckert, B., H\u00e4hnle, R. (eds.) TAP 2008. LNCS, vol.\u00a04966, pp. 154\u2013170. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24312-2_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T19:27:42Z","timestamp":1559244462000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24312-2_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319243115","9783319243122"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24312-2_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}