{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:56:46Z","timestamp":1762459006087},"publisher-location":"Berlin, Heidelberg","reference-count":41,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642340048"},{"type":"electronic","value":"9783642340055"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-34005-5_3","type":"book-chapter","created":{"date-parts":[[2012,10,2]],"date-time":"2012-10-02T22:33:39Z","timestamp":1349217219000},"page":"31-53","source":"Crossref","is-referenced-by-count":10,"title":["$\\mathbb{K}$ Framework Distilled"],"prefix":"10.1007","author":[{"given":"Dorel","family":"Lucanu","sequence":"first","affiliation":[]},{"given":"Traian Florin","family":"\u015eerb\u0103nu\u0163\u0103","sequence":"additional","affiliation":[]},{"given":"Grigore","family":"Ro\u015fu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","unstructured":"Ro\u015fu, G.: CS322, Fall 2003 - Programming Language Design: Lecture Notes. Technical Report UIUCDCS-R-2003-2897, University of Illinos at Urbana Champaign. Lecture notes of a course taught at UIUC (December 2003)"},{"issue":"6","key":"3_CR2","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1016\/j.jlap.2010.03.012","volume":"79","author":"G. Ro\u015fu","year":"2010","unstructured":"Ro\u015fu, G., \u015eerb\u0103nu\u0163\u0103, T.F.: An overview of the K semantic framework. Journal of Logic and Algebraic Programming\u00a079(6), 397\u2013434 (2010)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"3_CR3","unstructured":"Serbanuta, T.F., Arusoaie, A., Lazar, D., Ellison, C., Lucanu, D., Rosu, G.: The K primer (version 2.5). In: Hills, M. (ed.) Proceedings of the Second International K Workshop, K 2011. Electronic Notes in Theoretical Computer Science (to appear, 2012)"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude - A High-Performance Logical Framework","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 - A High-Performance Logical Framework. LNCS, vol.\u00a04350. Springer, Heidelberg (2007)"},{"key":"3_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-25984-8_1","volume-title":"Automated Reasoning","author":"J. Meseguer","year":"2004","unstructured":"Meseguer, J., Ro\u015fu, G.: Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097, pp. 1\u201344. Springer, Heidelberg (2004)"},{"issue":"3","key":"3_CR6","first-page":"213","volume":"373","author":"J. Meseguer","year":"2007","unstructured":"Meseguer, J., Ro\u015fu, G.: The rewriting logic semantics project. The rewriting logic semantics project\u00a0373(3), 213\u2013237 (2007)","journal-title":"The rewriting logic semantics project"},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-22953-4_1","volume-title":"Fundamentals of Computation Theory","author":"J. Meseguer","year":"2011","unstructured":"Meseguer, J., Ro\u015fu, G.: The Rewriting Logic Semantics Project: A Progress Report. In: Owe, O., Steffen, M., Telle, J.A. (eds.) FCT 2011. LNCS, vol.\u00a06914, pp. 1\u201337. Springer, Heidelberg (2011)"},{"key":"3_CR8","unstructured":"Lucanu, D., \u015eerb\u0103nu\u0163\u0103, T.F.: Cink - an exercise of thinking in K. Technical Report TR12-03, Department of Computer Science, Alexandru Ioan Cuza University of Ia\u015fi (2012), http:\/\/thor.info.uaic.ro\/~tr\/tr.pl.cgi"},{"issue":"1","key":"3_CR9","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.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science\u00a096(1), 73\u2013155 (1992)","journal-title":"Theoretical Computer Science"},{"issue":"2-3","key":"3_CR10","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1016\/j.tcs.2008.04.040","volume":"403","author":"J. Meseguer","year":"2008","unstructured":"Meseguer, J., Palomino, M., Mart\u00ed-Oliet, N.: Equational abstractions. Theoretical Computer Science\u00a0403(2-3), 239\u2013264 (2008)","journal-title":"Theoretical Computer Science"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1007\/978-3-540-27813-9_46","volume-title":"Computer Aided Verification","author":"A. Farzan","year":"2004","unstructured":"Farzan, A., Chen, F., Meseguer, J., Ro\u015fu, G.: Formal Analysis of Java Programs in JavaFAN. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 501\u2013505. Springer, Heidelberg (2004)"},{"issue":"4","key":"3_CR12","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K. Havelund","year":"2000","unstructured":"Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. STTT\u00a02(4), 366\u2013381 (2000)","journal-title":"STTT"},{"key":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/3-540-61604-7_64","volume-title":"CONCUR \u201996: Concurrency Theory","author":"J. Meseguer","year":"1996","unstructured":"Meseguer, J.: Rewriting Logic as a Semantic Framework for Concurrency: a Progress Report. In: Montanari, U., Sassone, V. (eds.) CONCUR 1996. LNCS, vol.\u00a01119, pp. 331\u2013372. Springer, Heidelberg (1996)"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Verdejo, A., Mart\u00ed-Oliet, N.: Implementing CCS in Maude 2. In: Gadducci, F., Montanari, U. (eds.) Proceedings of the Forth International Workshop on Rewriting Logic and its Applications (WRLA 2002). Electronic Notes in Theoretical Computer Science, vol. 71. Elsevier (2002)","DOI":"10.1016\/S1571-0661(05)82540-X"},{"key":"3_CR15","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1016\/j.ic.2008.03.026","volume":"207","author":"T.F. \u015eerb\u0103nu\u0163\u0103","year":"2009","unstructured":"\u015eerb\u0103nu\u0163\u0103, T.F., Ro\u015fu, G., Meseguer, J.: A rewriting logic approach to operational semantics. Information and Computation\u00a0207, 305\u2013340 (2009)","journal-title":"Information and Computation"},{"key":"3_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/BFb0039592","volume-title":"STACS 87","author":"G. Kahn","year":"1987","unstructured":"Kahn, G.: Natural Semantics. In: Brandenburg, F.J., Vidal-Naquet, G., Wirsing, M. (eds.) STACS 1987. LNCS, vol.\u00a0247, pp. 22\u201339. Springer, Heidelberg (1987)"},{"key":"3_CR17","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/j.jlap.2004.05.001","volume":"60-61","author":"G.D. Plotkin","year":"2004","unstructured":"Plotkin, G.D.: A structural approach to operational semantics. Journal of Logic and Algebraic Programming\u00a060-61, 17\u2013139 (2004); Original version: University of Aarhus Technical Report DAIMI FN-19 (1981)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"3_CR18","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1016\/j.jlap.2004.03.008","volume":"60-61","author":"P.D. Mosses","year":"2004","unstructured":"Mosses, P.D.: Modular structural operational semantics. Journal of Logic and Algebraic Programming\u00a060-61, 195\u2013228 (2004)","journal-title":"Journal of Logic and Algebraic Programming"},{"issue":"1","key":"3_CR19","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1006\/inco.1994.1093","volume":"115","author":"A.K. Wright","year":"1994","unstructured":"Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Information and Computation\u00a0115(1), 38\u201394 (1994)","journal-title":"Information and Computation"},{"key":"3_CR20","volume-title":"Essentials of Programming Languages","author":"D.P. Friedman","year":"2001","unstructured":"Friedman, D.P., Wand, M., Haynes, C.T.: Essentials of Programming Languages, 2nd edn. MIT Press, Cambridge (2001)","edition":"2"},{"issue":"1","key":"3_CR21","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. Theoretical Computer Science\u00a096(1), 217\u2013248 (1992)","journal-title":"Theoretical Computer Science"},{"key":"#cr-split#-3_CR22.1","doi-asserted-by":"crossref","unstructured":"Danvy, O., Nielsen, L.R.: Refocusing in reduction semantics. RS RS-04-26, BRICS, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark (November 2004)","DOI":"10.7146\/brics.v11i26.21851"},{"key":"#cr-split#-3_CR22.2","unstructured":"This report supersedes BRICS report RS-02-04. A preliminary version appears in the Informal Proceedings of the Second International Workshop on Rule-Based Programming, RULE 2001. Electronic Notes in Theoretical Computer Science, vol. 59.4"},{"key":"3_CR23","unstructured":"\u015eerb\u0103nu\u0163\u0103, T.F.: A Rewriting Approach to Concurrent Programming Language Design and Semantics. PhD thesis, University of Illinois at Urbana-Champaign (December 2010), https:\/\/www.ideals.illinois.edu\/handle\/2142\/18252"},{"key":"3_CR24","series-title":"LNCS","first-page":"83","volume-title":"WRLA 2012","author":"A. Arusoaie","year":"2012","unstructured":"Arusoaie, A., \u015eerb\u0103nu\u0163\u0103, T.F., Ellison, C., Ro\u015fu, G.: Making Maude Definitions More Interactive. In: Dur\u00e1n, F. (ed.) WRLA 2012. LNCS, vol.\u00a07571, pp. 83\u201398. Springer, Heidelberg (2012)"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Ellison, C., Ro\u015fu, G.: An executable formal semantics of C with applications. In: Proceedings of the 39th Symposium on Principles of Programming Languages (POPL 2012), pp. 533\u2013544. ACM (2012)","DOI":"10.1145\/2103656.2103719"},{"key":"3_CR26","unstructured":"Regehr, J., Chen, Y., Cuoq, P., Eide, E., Ellison, C., Yang, X.: Test-case reduction for C compiler bugs. In: 33nd Conference on Programming Language Design and Implementation (PLDI 2012). ACM (to appear, 2012)"},{"key":"3_CR27","unstructured":"Meredith, P., Hills, M., Ro\u015fu, G.: An executable rewriting logic semantics of k-scheme. In: Dube, D. (ed.) Proceedings of the 2007 Workshop on Scheme and Functional Programming, SCHEME 2007, Technical Report DIUL-RT-0701, Laval University, pp. 91\u2013103 (2007)"},{"key":"3_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-642-31762-0_14","volume-title":"Formal Verification of Object-Oriented Software","author":"V. Rusu","year":"2012","unstructured":"Rusu, V., Lucanu, D.: A K-Based Formal Framework for Domain-Specific Modelling Languages. In: Beckert, B., Damiani, F., Gurov, D. (eds.) FoVeOOS 2011. LNCS, vol.\u00a07421, pp. 214\u2013231. Springer, Heidelberg (2012)"},{"key":"3_CR29","unstructured":"Rusu, V., Lucanu, D.: K semantics for OCL\u2014a proposal for a formal definition for OCL. In: Hills, M. (ed.) Proceedings of the Second International K Workshop, K 2011. Electronic Notes in Theoretical Computer Science (to appear, 2012)"},{"key":"3_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1007\/978-3-540-95885-7_26","volume-title":"Membrane Computing","author":"T. \u015eerb\u0103nu\u0163\u0103","year":"2009","unstructured":"\u015eerb\u0103nu\u0163\u0103, T., \u015etef\u0103nescu, G., Ro\u015fu, G.: Defining and Executing P Systems with Structured Data in K. In: Corne, D.W., Frisco, P., P\u0103un, G., Rozenberg, G., Salomaa, A. (eds.) WMC 2008. LNCS, vol.\u00a05391, pp. 374\u2013393. Springer, Heidelberg (2009)"},{"key":"3_CR31","unstructured":"Asavoae, M.: K semantics for assembly languages: A case study. In: Hills, M. (ed.) Proceedings of the Second International K Workshop, K 2011. Electronic Notes in Theoretical Computer Science (to appear, 2012)"},{"key":"3_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-03429-9_10","volume-title":"Recent Trends in Algebraic Development Techniques","author":"C. Ellison","year":"2009","unstructured":"Ellison, C., \u015eerb\u0103nu\u0163\u0103, T.F., Ro\u015fu, G.: A Rewriting Logic Approach to Type Inference. In: Corradini, A., Montanari, U. (eds.) WADT 2008. LNCS, vol.\u00a05486, pp. 135\u2013151. Springer, Heidelberg (2009)"},{"key":"3_CR33","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":"3_CR34","doi-asserted-by":"crossref","unstructured":"Ro\u015fu, G., \u015etef\u0103nescu, A.: Matching logic: A new program verification approach (NIER track). In: 30th International Conference on Software Engineering (ICSE 2011), pp. 868\u2013871 (2011)","DOI":"10.1145\/1985793.1985928"},{"key":"3_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-642-16310-4_9","volume-title":"Rewriting Logic and Its Applications","author":"I.M. As\u0103voae","year":"2010","unstructured":"As\u0103voae, I.M., As\u0103voae, M.: Collecting Semantics under Predicate Abstraction in the K Framework. In: \u00d6lveczky, P.C. (ed.) WRLA 2010. LNCS, vol.\u00a06381, pp. 123\u2013139. Springer, Heidelberg (2010)"},{"key":"3_CR36","doi-asserted-by":"crossref","unstructured":"Asavoae, I.M., de Boer, F., Bonsangue, M.M., Lucanu, D., Rot, J.: Bounded model checking of recursive programs with pointers in k. In: WRLA (2012); as extended abstract in the ETAPS preproceedings","DOI":"10.1007\/978-3-642-37635-1_4"},{"key":"3_CR37","doi-asserted-by":"crossref","unstructured":"Asavoae, I.M., Asavoae, M., Lucanu, D.: Path directed symbolic execution in the k framework. In: Ida, T., Negru, V., Jebelean, T., Petcu, D., Watt, S.M., Zaharie, D. (eds.) SYNASC, pp. 133\u2013141. IEEE Computer Society (2010)","DOI":"10.1109\/SYNASC.2010.78"},{"key":"3_CR38","unstructured":"Asavoae, I.M.: Abstract semantics for alias analysis in K. In: Hills, M. (ed.) K 2011. Electronic Notes in Theoretical Computer Science (to appear, 2012)"},{"key":"3_CR39","unstructured":"As\u0103voae, M., Lucanu, D., Ro\u015fu, G.: Towards semantics-based WCET analysis. In: WCET (2011)"},{"key":"3_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-642-04694-0_10","volume-title":"Runtime Verification","author":"G. Ro\u015fu","year":"2009","unstructured":"Ro\u015fu, G., Schulte, W., \u015eerb\u0103nu\u0163\u0103, T.F.: Runtime Verification of C Memory Safety. In: Bensalem, S., Peled, D.A. (eds.) RV 2009. LNCS, vol.\u00a05779, pp. 132\u2013151. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Rewriting Logic and Its Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-34005-5_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,29]],"date-time":"2022-01-29T17:46:52Z","timestamp":1643478412000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-34005-5_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642340048","9783642340055"],"references-count":41,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-34005-5_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}