{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,16]],"date-time":"2026-06-16T23:08:15Z","timestamp":1781651295148,"version":"3.54.5"},"publisher-location":"Cham","reference-count":9,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319335995","type":"print"},{"value":"9783319336008","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-33600-8_15","type":"book-chapter","created":{"date-parts":[[2016,5,10]],"date-time":"2016-05-10T04:15:15Z","timestamp":1462853715000},"page":"237-243","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Relational Encoding for a Clash-Free Subset of ASMs"],"prefix":"10.1007","author":[{"given":"Gerhard","family":"Schellhorn","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gidon","family":"Ernst","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"J\u00f6rg","family":"Pf\u00e4hler","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Wolfgang","family":"Reif","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,5,11]]},"reference":[{"key":"15_CR1","unstructured":"B\u00f6rger, E., Rosenzweig, D.: The WAM\u2013definition, compiler correctness. In: Logic Programming: Formal Methods and Practical Applications, Studies in Computer Science and Artificial Intelligence, vol. 11, pp. 20\u201390. Elsevier (1995)"},{"key":"15_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18216-7","volume-title":"Abstract State Machines\u2013a Method for High-level System Design and Analysis","author":"E B\u00f6rger","year":"2003","unstructured":"B\u00f6rger, E., St\u00e4rk, R.F.: Abstract State Machines\u2013a Method for High-level System Design and Analysis. Springer, Heidelberg (2003)"},{"issue":"6","key":"15_CR3","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1007\/s10009-014-0308-3","volume":"17","author":"G Ernst","year":"2015","unstructured":"Ernst, G., Pf\u00e4hler, J., Schellhorn, G., Haneberg, D., Reif, W.: KIV - overview and VerifyThis competition. Softw. Tools Techn. Transfer 17(6), 677\u2013694 (2015)","journal-title":"Softw. Tools Techn. Transfer"},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-319-30024-5_18","volume-title":"Foundations of Information and Knowledge Systems","author":"F Ferrarotti","year":"2016","unstructured":"Ferrarotti, F., Schewe, K.-D., Tec, L., Wang, Q.: A logic for non-deterministic parallel Abstract State Machines. In: Gyssens, M. (ed.) FoIKS 2016. LNCS, vol. 9616, pp. 334\u2013354. Springer, Heidelberg (2016). doi:\n                      10.1007\/978-3-319-30024-5_18"},{"key":"15_CR5","first-page":"119","volume-title":"Lecture Notes in Computer Science","author":"Michael Leuschel","year":"2016","unstructured":"Leuschel, M., B\u00f6rger, E.: A compact encoding of sequential ASMs in Event-B. In: Butler, M., Schewe, K.D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 119\u2013134. Springer, Heidelberg (2016)"},{"key":"15_CR6","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/s10472-013-9389-z","volume":"71","author":"G Schellhorn","year":"2014","unstructured":"Schellhorn, G., Tofan, B., Ernst, G., Pf\u00e4hler, J., Reif, W.: RGITL: a temporal logic framework for compositional reasoning about interleaved programs. Ann. Math. Artif. Int. (AMAI) 71, 131\u2013174 (2014)","journal-title":"Ann. Math. Artif. Int. (AMAI)"},{"issue":"11","key":"15_CR7","first-page":"981","volume":"7","author":"RF St\u00e4rk","year":"2001","unstructured":"St\u00e4rk, R.F., Nanchen, S.: A complete logic for Abstract State Machines. J. Univ. Comput. Sci. (J.UCS) 7(11), 981\u20131006 (2001)","journal-title":"J. Univ. Comput. Sci. (J.UCS)"},{"key":"15_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59495-3","volume-title":"Java and the Java Virtual Machine: Definition, Verification","author":"RF St\u00e4rk","year":"2001","unstructured":"St\u00e4rk, R.F., Schmid, J., B\u00f6rger, E.: Java and the Java Virtual Machine: Definition, Verification. Springer, Validation (2001)"},{"key":"15_CR9","unstructured":"A relational encoding for a clash-free subset of ASMs: Formalization and proofs. \n                      https:\/\/swt.informatik.uni-augsburg.de\/swt\/projects\/Refinement\/ASM-clashfreedom.html"}],"container-title":["Lecture Notes in Computer Science","Abstract State Machines, Alloy, B, TLA, VDM, and Z"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-33600-8_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T23:22:40Z","timestamp":1559431360000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-33600-8_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319335995","9783319336008"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-33600-8_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"11 May 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}