{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T15:10:09Z","timestamp":1748790609807,"version":"3.41.0"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319302454"},{"type":"electronic","value":"9783319302461"}],"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-30246-1_7","type":"book-chapter","created":{"date-parts":[[2016,2,26]],"date-time":"2016-02-26T08:47:59Z","timestamp":1456476479000},"page":"109-123","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Abstracting an Operational Semantics to Finite Automata"],"prefix":"10.1007","author":[{"given":"Nadezhda","family":"Baklanova","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wilmer","family":"Ricciotti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan-Georg","family":"Smaus","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Strecker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,2,27]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking for real-time systems. In: LICS, pp. 414\u2013425. IEEE Computer Society (1990)","DOI":"10.1109\/LICS.1990.113766"},{"key":"7_CR2","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126, 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-540-74591-4_3","volume-title":"Theorem Proving in Higher Order Logics","author":"AW Appel","year":"2007","unstructured":"Appel, A.W., Blazy, S.: Separation logic for small-step cminor. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 5\u201321. Springer, Heidelberg (2007)"},{"key":"7_CR4","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"7_CR5","unstructured":"Baklanova, N.: Semantics and Proof Methods for a Real-Time Modeling Language. PhD thesis, Universit\u00e9 de Toulouse (2014)"},{"key":"7_CR6","unstructured":"Baklanova, N., Ricciotti, W., Smaus, J.-G., Strecker, M.: Abstracting an operational semantics to finite automata (formalization) (2014). https:\/\/bitbucket.org\/Martin_Strecker\/abstracting_op_sem_to_automata"},{"key":"7_CR7","unstructured":"Baklanova, N., Ricciotti, W., Smaus, J.-G., Strecker, M.: Abstracting an operational semantics to finite automata. In: Proceedings of the 11th International Conference on ICT in Education, Research and Industrial Applications: Integration, Harmonization and Knowledge Transfer, Lviv, Ukraine, 14\u201316 May 2015, pp. 354\u2013365 (2015)"},{"key":"7_CR8","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-35737-4_1","volume-title":"ICT in Education, Research, and Industrial Applications","author":"N Baklanova","year":"2013","unstructured":"Baklanova, N., Strecker, M.: Abstraction and verification of properties of a real-time java. In: Ermolayev, V., Mayr, H.C., Nikitchenko, M., Spivakovsky, A., Zholtkevych, G. (eds.) ICTERI 2012. CCIS, vol. 347, pp. 1\u201318. Springer, Heidelberg (2013)"},{"key":"7_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-540-27755-2_3","volume-title":"Lectures on Concurrency and Petri Nets","author":"JE Bengtsson","year":"2004","unstructured":"Bengtsson, J.E., Yi, W.: Timed automata: semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 87\u2013124. Springer, Heidelberg (2004)"},{"issue":"5","key":"7_CR10","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1017\/S0956796897002864","volume":"7","author":"G Huet","year":"1997","unstructured":"Huet, G.: Functional pearl: the zipper. J. Funct. Program. 7(5), 549\u2013554 (1997)","journal-title":"J. Funct. Program."},{"key":"7_CR11","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0171-7","volume-title":"Automata Theory and Its Applications","author":"B Khoussainov","year":"2001","unstructured":"Khoussainov, B., Nerode, A.: Automata Theory and Its Applications. Birkhauser, Boston (2001)"},{"key":"7_CR12","doi-asserted-by":"publisher","first-page":"619","DOI":"10.1145\/1146809.1146811","volume":"28","author":"G Klein","year":"2006","unstructured":"Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine, and compiler. ACM Trans. Program. Lang. Syst. 28, 619\u2013695 (2006)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"7_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/978-3-642-37075-5_17","volume-title":"Foundations of Software Science and Computation Structures","author":"R Krebbers","year":"2013","unstructured":"Krebbers, R., Wiedijk, F.: Separation logic for non-local control flow and block scope variables. In: Pfenning, F. (ed.) FOSSACS 2013 (ETAPS 2013). LNCS, vol. 7794, pp. 257\u2013272. Springer, Heidelberg (2013)"},{"issue":"4","key":"7_CR14","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: A formally verified compiler back-end. J. Autom. Reasoning 43(4), 363\u2013446 (2009)","journal-title":"J. Autom. Reasoning"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, vol. 2283. Springer, Heidelberg (2002)"},{"key":"7_CR16","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3054.001.0001","volume-title":"The Formal Semantics of Programming Languages: An Introduction","author":"G Winskel","year":"1993","unstructured":"Winskel, G.: The Formal Semantics of Programming Languages: An Introduction. MIT Press, Cambridge (1993)"}],"container-title":["Communications in Computer and Information Science","Information and Communication Technologies in Education, Research, and Industrial Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-30246-1_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T14:44:58Z","timestamp":1748789098000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-30246-1_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319302454","9783319302461"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-30246-1_7","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"27 February 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}