{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:46:42Z","timestamp":1742914002226,"version":"3.40.3"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319899596"},{"type":"electronic","value":"9783319899602"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-89960-2_4","type":"book-chapter","created":{"date-parts":[[2018,4,11]],"date-time":"2018-04-11T10:14:43Z","timestamp":1523441683000},"page":"61-78","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":22,"title":["Verified Model Checking of Timed Automata"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5998-4655","authenticated-orcid":false,"given":"Simon","family":"Wimmer","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3576-0504","authenticated-orcid":false,"given":"Peter","family":"Lammich","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,4,12]]},"reference":[{"issue":"2","key":"4_CR1","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. Theoret. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theoret. Comput. Sci."},{"key":"4_CR2","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":"J Bengtsson","year":"2004","unstructured":"Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 87\u2013124. Springer, Heidelberg (2004). \n https:\/\/doi.org\/10.1007\/978-3-540-27755-2_3"},{"key":"4_CR3","doi-asserted-by":"publisher","first-page":"620","DOI":"10.1007\/3-540-36494-3_54","volume-title":"Lecture Notes in Computer Science","author":"Patricia Bouyer","year":"2003","unstructured":"Bouyer, P.: Untameable timed automata! In: Alt, H., Habib, M. (eds.) STACS 2003. LNCS, vol. 2607, pp. 620\u2013631. Springer, Heidelberg (2003). \n https:\/\/doi.org\/10.1007\/3-540-36494-3_54"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). \n https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"166","DOI":"10.1007\/978-3-642-32347-8_12","volume-title":"Interactive Theorem Proving","author":"P Lammich","year":"2012","unstructured":"Lammich, P., Tuerk, T.: Applying data refinement for monadic programs to Hopcroft\u2019s algorithm. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 166\u2013182. Springer, Heidelberg (2012). \n https:\/\/doi.org\/10.1007\/978-3-642-32347-8_12"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-319-22102-1_17","volume-title":"Interactive Theorem Proving","author":"P Lammich","year":"2015","unstructured":"Lammich, P.: Refinement to Imperative\/HOL. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 253\u2013269. Springer, Cham (2015). \n https:\/\/doi.org\/10.1007\/978-3-319-22102-1_17"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/978-3-319-43144-4_26","volume-title":"Interactive Theorem Proving","author":"S Wimmer","year":"2016","unstructured":"Wimmer, S.: Formalized timed automata. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 425\u2013440. Springer, Cham (2016). \n https:\/\/doi.org\/10.1007\/978-3-319-43144-4_26"},{"key":"4_CR8","unstructured":"Xu, Q., Miao, H.: Formal verification framework for safety of real-time system based on timed automata model in PVS. In: Proceedings of the IASTED International Conference on Software Engineering, pp. 107\u2013112 (2006)"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Xu, Q., Miao, H.: Manipulating clocks in timed automata using PVS. In: Proceedings of SNPD 2009, pp. 555\u2013560 (2009)","DOI":"10.1109\/SNPD.2009.69"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/3-540-45500-0_15","volume-title":"Theoretical Aspects of Computer Software","author":"C Paulin-Mohring","year":"2001","unstructured":"Paulin-Mohring, C.: Modelisation of timed automata in Coq. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol. 2215, pp. 298\u2013315. Springer, Heidelberg (2001). \n https:\/\/doi.org\/10.1007\/3-540-45500-0_15"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/978-3-642-40229-6_8","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"M Garnacho","year":"2013","unstructured":"Garnacho, M., Bodeveix, J.-P., Filali-Amine, M.: A mechanized semantic framework for real-time systems. In: Braberman, V., Fribourg, L. (eds.) FORMATS 2013. LNCS, vol. 8053, pp. 106\u2013120. Springer, Heidelberg (2013). \n https:\/\/doi.org\/10.1007\/978-3-642-40229-6_8"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: Proceedings of the Twenty-Fifth Annual ACM Symposium on Theory of Computing, pp. 592\u2013601 (1993)","DOI":"10.1145\/167088.167242"},{"key":"4_CR13","unstructured":"Cast\u00e9ran, P., Rouillard, D.: Towards a generic tool for reasoning about labeled transition systems. In: TPHOLs 2001: Supplemental Proceedings (2001). \n http:\/\/www.informatics.ed.ac.uk\/publications\/report\/0046.html"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/BFb0054171","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Sprenger","year":"1998","unstructured":"Sprenger, C.: A verified model checker for the modal \n \n \n \n $$\\mu $$\n -calculus in Coq. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 167\u2013183. Springer, Heidelberg (1998). \n https:\/\/doi.org\/10.1007\/BFb0054171"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/978-3-642-39799-8_31","volume-title":"Computer Aided Verification","author":"J Esparza","year":"2013","unstructured":"Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.-G.: A fully verified executable LTL model checker. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 463\u2013478. Springer, Heidelberg (2013). \n https:\/\/doi.org\/10.1007\/978-3-642-39799-8_31"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-3-319-12154-3_7","volume-title":"Verified Software: Theories, Tools and Experiments","author":"R Neumann","year":"2014","unstructured":"Neumann, R.: Using promela in a fully verified executable LTL model checker. In: Giannakopoulou, D., Kroening, D. (eds.) VSTTE 2014. LNCS, vol. 8471, pp. 105\u2013114. Springer, Cham (2014). \n https:\/\/doi.org\/10.1007\/978-3-319-12154-3_7"},{"issue":"1","key":"4_CR17","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10817-017-9418-4","volume":"60","author":"J Brunner","year":"2018","unstructured":"Brunner, J., Lammich, P.: Formal verification of an executable LTL model checker with partial order reduction. J. Autom. Reasoning 60(1), 3\u201321 (2018)","journal-title":"J. Autom. Reasoning"},{"key":"4_CR18","unstructured":"Herbreteau, F., Srivathsan, B., Tran, T.T., Walukiewicz, I.: Why liveness for timed automata is hard, and what we can do about it. In: Lal, A., Akshay, S., Saurabh, S., Sen, S. (eds.) FSTTCS 2016, vol. 65. LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, pp. 48:1\u201348:14 (2016)"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-319-03545-1_9","volume-title":"Certified Programs and Proofs","author":"B Huffman","year":"2013","unstructured":"Huffman, B., Kun\u010dar, O.: Lifting and transfer: a modular design for quotients in Isabelle\/HOL. In: Gonthier, G., Norrish, M. (eds.) CPP 2013. LNCS, vol. 8307, pp. 131\u2013146. Springer, Cham (2013). \n https:\/\/doi.org\/10.1007\/978-3-319-03545-1_9"},{"key":"4_CR20","unstructured":"Bouajjani, A., Tripakis, S., Yovine, S.: On-the-fly symbolic model checking for real-time systems. In: Proceedings of the 18th IEEE Real-Time Systems Symposium (RTSS 1997), 3\u20135 December 1997, San Francisco, CA, USA, pp. 25\u201334 (1997)"},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11603009_7","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"G Behrmann","year":"2005","unstructured":"Behrmann, G., Larsen, K.G., Rasmussen, J.I.: Beyond liveness: efficient parameter synthesis for time bounded liveness. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 81\u201394. Springer, Heidelberg (2005). \n https:\/\/doi.org\/10.1007\/11603009_7"},{"key":"4_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-540-71067-7_14","volume-title":"Theorem Proving in Higher Order Logics","author":"L Bulwahn","year":"2008","unstructured":"Bulwahn, L., Krauss, A., Haftmann, F., Erk\u00f6k, L., Matthews, J.: Imperative functional programming with Isabelle\/HOL. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 134\u2013149. Springer, Heidelberg (2008). \n https:\/\/doi.org\/10.1007\/978-3-540-71067-7_14"},{"key":"4_CR23","doi-asserted-by":"publisher","unstructured":"Chargu\u00e9raud, A.: Higher-order representation predicates in separation logic. In: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2016, St. Petersburg, FL, USA, pp. 2\u201314. ACM, New York (2016). \n https:\/\/doi.org\/10.1145\/2854065.2854068","DOI":"10.1145\/2854065.2854068"},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-12251-4_9","volume-title":"Functional and Logic Programming","author":"F Haftmann","year":"2010","unstructured":"Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol. 6009, pp. 103\u2013117. Springer, Heidelberg (2010). \n https:\/\/doi.org\/10.1007\/978-3-642-12251-4_9"},{"key":"4_CR25","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-319-89960-2_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Simon Wimmer","year":"2018","unstructured":"Wimmer, S., Lammich, P.: Verified model checking of timed automata - artifact (2018)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-89960-2_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,3]],"date-time":"2020-03-03T03:14:33Z","timestamp":1583205273000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89960-2_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319899596","9783319899602"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89960-2_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"12 April 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Thessaloniki","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 April 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 April 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/index.php\/2018\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}