{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:23:54Z","timestamp":1725488634702},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540664635"},{"type":"electronic","value":"9783540482567"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","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":[[1999]]},"DOI":"10.1007\/3-540-48256-3_18","type":"book-chapter","created":{"date-parts":[[2007,8,3]],"date-time":"2007-08-03T16:15:22Z","timestamp":1186157722000},"page":"273-289","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["From I\/O Automata to Timed I\/O Automata"],"prefix":"10.1007","author":[{"given":"Bernd","family":"Grobauer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Olaf","family":"M\u00fcller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,9,17]]},"reference":[{"key":"18_CR1","unstructured":"The isabelle theories for timed i\/o automata and the Generalized Railroad Crossing. available via \n                  http:\/\/www.brics.dk\/~grobauer\/tioa\/index.html\n                  \n                ."},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"Myla M. Archer and Constance L. Heitmeyer. Mechanical verification of timed automata: A case study. Technical Report NRL\/MR\/5546-98-8180, Naval Research Laboratory, 1998.","DOI":"10.21236\/ADA359891"},{"key":"18_CR3","unstructured":"Myla M. Archer, Constance L. Heitmeyer, and Steve Sims. TAME: A PVS interface to simplify proofs for automata models. In Proceedings of UITP\u2019 98, July 1998."},{"key":"18_CR4","unstructured":"Stefan Berghofer. Definitorische Konstruktion induktiver Datentypen in Isabelle\/HOL. Master\u2019s thesis, TU M\u00fcnchen, 1998."},{"issue":"9","key":"18_CR5","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1109\/32.58786","volume":"16","author":"A. J. Camilleri","year":"1990","unstructured":"Albert J. Camilleri. Mechanizing CSP trace theory in higher order logic. IEEE Transactions on Software Engineering, 16(9):993\u20131004, 1990.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"18_CR6","series-title":"Lect Notes Comput Sci","volume-title":"Proc. 2nd Workshop Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201996)","author":"C.-T. Chou","year":"1996","unstructured":"Ching-Tsun Chou and Doron Peled. Formal verification of a partial-order reduction technique for model checking. In T. Margaria and B. Steffen, editors, Proc. 2nd Workshop Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201996), volume 1055 of Lecture Notes in Computer Science. Springer Verlag, 1996."},{"key":"18_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/BFb0028388","volume-title":"TPHOL\u201997, Proc. of the 10th International Workshop on Theorem Proving in Higher Order Logics","author":"M. Devillers","year":"1997","unstructured":"Marco Devillers, David Griffioen, and Olaf M\u00fcller. Possibly infinite sequences in theorem provers: A comparative study. In TPHOL\u201997, Proc. of the 10th International Workshop on Theorem Proving in Higher Order Logics, volume 1275 of Lecture Notes in Computer Science, pages 89\u2013104, 1997."},{"key":"18_CR8","volume-title":"Technical report, Laboratory for Computer Science","author":"R. Gawlick","year":"1993","unstructured":"R. Gawlick, R. Segala, J.F. Sogaard-Andersen, and N.A. Lynch. Liveness in timed and untimed systems. Technical report, Laboratory for Computer Science, MIT, Cambridge, MA., December 1993. Extended abstract in Proceedings ICALP\u2019 94."},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"Constance Heitmeyer and Nancy Lynch. The generalized railroad crossing: A case study in formal verification of real-time systems. In Proceedings of the IEEE Real-Time Systems Symposium, San Juan, Puerto Rico, Dec. 1994.","DOI":"10.1109\/REAL.1994.342724"},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"N.A. Lynch and F.W. Vaandrager. Forward and backward simulations \u2014 Part II: timing based systems. Technical Report CS-R9314, CWI, 1993.","DOI":"10.1007\/BFb0032002"},{"key":"18_CR11","unstructured":"Nancy A. Lynch. Distributed Algorithms. Morgan Kaufmann Publishers, 1996."},{"key":"18_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/BFb0055145","volume-title":"TPHOL\u201998. Proc. of the 11th International Workshop on Theorem Proving in Higher Order Logics","author":"O. M\u00fcller","year":"1998","unstructured":"Olaf M\u00fcller. I\/O Automata and Beyond \u2014 Temporal Logic and Abstraction in Isabelle. In TPHOL\u201998. Proc. of the 11th International Workshop on Theorem Proving in Higher Order Logics, volume 1479 of Lecture Notes in Computer Science, pages 331\u2013348, 1998."},{"key":"18_CR13","unstructured":"Olaf M\u00fcller. A Verification Environment for I\/O Automata Based on Formalized Meta-Theory. PhD thesis, TUM\u00fcnchen, 1998."},{"key":"18_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"580","DOI":"10.1007\/BFb0030627","volume-title":"TAPSOFT\u201997: Theory and Practice of Software Development","author":"O. M\u00fcller","year":"1997","unstructured":"Olaf M\u00fcller and Tobias Nipkow. Traces of I\/O automata in Isabelle\/HOLCF. In M. Bidoit and M. Dauchet, editors, TAPSOFT\u201997: Theory and Practice of Software Development, volume 1214 of LNCS, pages 580\u2013594. Springer, 1997."},{"key":"18_CR15","unstructured":"Olaf M\u00fcller, Tobias Nipkow, David von Oheimb, and Oscar Slotosch. HOLCF = HOL + LCF. To appear in Journal of Functional Programming."},{"key":"18_CR16","series-title":"Lect Notes Comput Sci","volume-title":"Theorem Proving in Higher Order Logics, Proceedings of TPHOLs\u2019 98","author":"W. Naraschewski","year":"1998","unstructured":"Wolfgang Naraschewski and Markus Wenzel. Object-oriented verification based on record subtyping in higher-order logic. In Theorem Proving in Higher Order Logics, Proceedings of TPHOLs\u2019 98, volume 1479 of Lecture Notes in Computer Science, 1998."},{"key":"18_CR17","first-page":"161","volume-title":"Proc. 25th ACM Symp. Principles of Programming Languages","author":"T. Nipkow","year":"1998","unstructured":"Tobias Nipkow and David von Oheimb. Javalight is type-safe \u2014 definitely. In Proc. 25th ACM Symp. Principles of Programming Languages, pages 161\u2013170. ACM Press, New York, 1998."},{"key":"18_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61474-5_91","volume-title":"Computer Aided Verification","author":"S. Owre","year":"1996","unstructured":"S. Owre, Rushby J., Shankar N., and M. Srivas. PVS: Combining specification, proof checking, and model checking. In R. Alur and T.A. Henzinger, editors, Computer Aided Verification, volume 1102 of Lecture Notes in Computer Science, 1996."},{"key":"18_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L. C. Paulson","year":"1994","unstructured":"Lawrence C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer Verlag, 1994."},{"key":"18_CR20","unstructured":"Lawrence C. Paulson. Generic automatic proof tools. In R. Veroff, editor, Automated Reasoning and its Applications. MIT Press, 1997."},{"key":"18_CR21","unstructured":"Lawrence C. Paulson. A generic tableau prover and its integration with Isabelle. In CADE-15 Workshop on Integration of Deductive Systems, 1998."},{"key":"18_CR22","series-title":"Lect Notes Comput Sci","volume-title":"In Theorem Proving in Higher Order Logics, Proceedings of TPHOLs\u2019 97","author":"M. Wenzel","year":"1997","unstructured":"Markus Wenzel. Type classes and overloading in higher-order logic. In Theorem Proving in Higher Order Logics, Proceedings of TPHOLs\u2019 97, volume 1275 of Lecture Notes in Computer Science, 1997."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48256-3_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T11:37:30Z","timestamp":1578483450000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48256-3_18"}},"subtitle":["A Solution to the \u2018Generalized Railroad Crossing\u2019 in Isabelle\/HOLCF"],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664635","9783540482567"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-48256-3_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]},"assertion":[{"value":"17 September 1999","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}