{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T10:11:14Z","timestamp":1781086274901,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642315848","type":"print"},{"value":"9783642315855","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31585-5_33","type":"book-chapter","created":{"date-parts":[[2012,6,23]],"date-time":"2012-06-23T07:56:29Z","timestamp":1340438189000},"page":"351-363","source":"Crossref","is-referenced-by-count":13,"title":["Towards a Unified Theory of Operational and Axiomatic Semantics"],"prefix":"10.1007","author":[{"given":"Grigore","family":"Ro\u015fu","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrei","family":"\u015etef\u0103nescu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"33_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-19718-5_1","volume-title":"Programming Languages and Systems","author":"A.W. Appel","year":"2011","unstructured":"Appel, A.W.: Verified Software Toolchain. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol.\u00a06602, pp. 1\u201317. Springer, Heidelberg (2011)"},{"key":"33_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":"33_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/11575467_5","volume-title":"Programming Languages and Systems","author":"J. Berdine","year":"2005","unstructured":"Berdine, J., Calcagno, C., O\u2019Hearn, P.W.: Symbolic Execution with Separation Logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol.\u00a03780, pp. 52\u201368. Springer, Heidelberg (2005)"},{"issue":"1","key":"33_CR4","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(92)90185-I","volume":"96","author":"G. Berry","year":"1992","unstructured":"Berry, G., Boudol, G.: The chemical abstract machine. Th. Comp. Sci.\u00a096(1), 217\u2013248 (1992)","journal-title":"Th. Comp. Sci."},{"key":"33_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude","author":"M. Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All About Maude. LNCS, vol.\u00a04350. Springer, Heidelberg (2007)"},{"key":"33_CR6","doi-asserted-by":"crossref","unstructured":"Ellison, C., Rosu, G.: An executable formal semantics of C with applications. In: POPL, pp. 533\u2013544. ACM (2012)","DOI":"10.1145\/2103656.2103719"},{"key":"33_CR7","unstructured":"Felleisen, M., Findler, R.B., Flatt, M.: Semantics Engineering with PLT Redex. MIT (2009)"},{"key":"33_CR8","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meaning to programs. In: Symposia in Applied Mathematics, vol.\u00a019, pp. 19\u201332. AMS (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"33_CR9","unstructured":"George, C., Haxthausen, A.E., Hughes, S., Milne, R., Prehn, S., Pedersen, J.S.: The RAISE Development Method. BCS Practitioner Series. Prentice Hall (1995)"},{"key":"33_CR10","doi-asserted-by":"crossref","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic logic. In: Handbook of Philosophical Logic, pp. 497\u2013604 (1984)","DOI":"10.1007\/978-94-009-6259-0_10"},{"issue":"10","key":"33_CR11","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM\u00a012(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"33_CR12","unstructured":"Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice Hall (1998)"},{"issue":"1-2","key":"33_CR13","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.jlap.2003.07.005","volume":"58","author":"B. Jacobs","year":"2004","unstructured":"Jacobs, B.: Weakest pre-condition reasoning for java programs with JML annotations. J. Log. Algebr. Program.\u00a058(1-2), 61\u201388 (2004)","journal-title":"J. Log. Algebr. Program."},{"issue":"2","key":"33_CR14","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1016\/j.ic.2007.12.004","volume":"207","author":"X. Leroy","year":"2009","unstructured":"Leroy, X., Grall, H.: Coinductive big-step operational semantics. Inf. Comput.\u00a0207(2), 284\u2013304 (2009)","journal-title":"Inf. Comput."},{"key":"33_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-540-30142-4_14","volume-title":"Theorem Proving in Higher Order Logics","author":"H. Liu","year":"2004","unstructured":"Liu, H., Moore, J.S.: Java Program Verification via a JVM Deep Embedding in ACL2. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol.\u00a03223, pp. 184\u2013200. Springer, Heidelberg (2004)"},{"issue":"1","key":"33_CR16","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J. Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditioned rewriting logic as a united model of concurrency. Theor. Comput. Sci.\u00a096(1), 73\u2013155 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"33_CR17","series-title":"Lecture Notes in Computer Science","volume-title":"CASL Reference Manual","year":"2004","unstructured":"Mosses, P.D. (ed.): CASL Reference Manual. LNCS, vol.\u00a02960. Springer, Heidelberg (2004)"},{"key":"33_CR18","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)"},{"key":"33_CR19","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/s001650050009","volume":"10","author":"T. Nipkow","year":"1998","unstructured":"Nipkow, T.: Winskel is (almost) right: Towards a mechanized semantics textbook. Formal Aspects of Computing\u00a010, 171\u2013186 (1998)","journal-title":"Formal Aspects of Computing"},{"key":"33_CR20","doi-asserted-by":"crossref","unstructured":"Pasareanu, C.S., Mehlitz, P.C., Bushnell, D.H., Gundy-Burlet, K., Lowry, M.R., Person, S., Pape, M.: Combining unit-level symbolic execution and system-level concrete execution for testing NASA software. In: ISSTA, pp. 15\u201326. ACM (2008)","DOI":"10.1145\/1390630.1390635"},{"key":"33_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-17796-5_9","volume-title":"Algebraic Methodology and Software Technology","author":"G. Ro\u015fu","year":"2011","unstructured":"Ro\u015fu, G., Ellison, C., Schulte, W.: Matching Logic: An Alternative to Hoare\/Floyd Logic. In: Johnson, M., Pavlovic, D. (eds.) AMAST 2010. LNCS, vol.\u00a06486, pp. 142\u2013162. Springer, Heidelberg (2011)"},{"key":"33_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-642-03741-2_10","volume-title":"Algebra and Coalgebra in Computer Science","author":"G. Ro\u015fu","year":"2009","unstructured":"Ro\u015fu, G., Lucanu, D.: Circular Coinduction: A Proof Theoretical Foundation. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol.\u00a05728, pp. 127\u2013144. Springer, Heidelberg (2009)"},{"issue":"6","key":"33_CR23","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1016\/j.jlap.2010.03.012","volume":"79","author":"G. Rosu","year":"2010","unstructured":"Rosu, G., Serbanuta, T.F.: An overview of the K semantic framework. J. Log. Algebr. Program.\u00a079(6), 397\u2013434 (2010)","journal-title":"J. Log. Algebr. Program."},{"key":"33_CR24","doi-asserted-by":"crossref","unstructured":"Rosu, G., Stefanescu, A.: Matching logic: A new program verification approach (NIER track). In: ICSE, pp. 868\u2013871. ACM (2011)","DOI":"10.1145\/1985793.1985928"},{"key":"33_CR25","unstructured":"Rosu, G., Stefanescu, A.: From Hoare logic to matching logic reachability. In: FM (to appear, 2012)"},{"key":"33_CR26","doi-asserted-by":"crossref","unstructured":"Rosu, G., Stefanescu, A.: Towards a unified theory of operational and axiomatic semantics. Tech. Rep., Univ. of Illinois (May 2012), http:\/\/hdl.handle.net\/2142\/30827","DOI":"10.1007\/978-3-642-31585-5_33"},{"issue":"4","key":"33_CR27","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/j.entcs.2007.06.006","volume":"176","author":"R. Sasse","year":"2007","unstructured":"Sasse, R., Meseguer, J.: Java+ITP: A verification tool based on Hoare logic and algebraic semantics. Electr. Notes Theor. Comput. Sci.\u00a0176(4), 29\u201346 (2007)","journal-title":"Electr. Notes Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Automata, Languages, and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31585-5_33.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,23]],"date-time":"2020-11-23T22:08:30Z","timestamp":1606169310000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31585-5_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642315848","9783642315855"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31585-5_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}