{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:44:29Z","timestamp":1725493469876},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540427360"},{"type":"electronic","value":"9783540455004"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45500-0_15","type":"book-chapter","created":{"date-parts":[[2007,10,25]],"date-time":"2007-10-25T15:37:33Z","timestamp":1193326653000},"page":"298-315","source":"Crossref","is-referenced-by-count":10,"title":["Modelisation of Timed Automata in Coq"],"prefix":"10.1007","author":[{"given":"Christine","family":"Paulin-Mohring","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,10,10]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 1994.","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"15_CR2","unstructured":"E. Beffara, O. Bournez, H. Kacem, and C. Kirchner. Verification of timed automata using rewrite rules and strategies. \n                    http:\/\/www.loria.fr\/~kacem\/AT\/timedautomata.ps.gz\n                    \n                  , 2001."},{"key":"15_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/3-540-48683-6_11","volume-title":"11th Int. Conf. Computer Aided Verification (CAV\u201999)","author":"B. B\u00e9rard","year":"1999","unstructured":"B. B\u00e9rard and L. Fribourg. Automated verification of a parametric real-time program: the abr conformance protocol. In 11th Int. Conf. Computer Aided Verification (CAV\u201999), number 1633 in Lecture Notes in Computer Science, pages 96\u2013107. Springer-Verlag, 1999."},{"key":"15_CR4","unstructured":"B. B\u00e9rard, L. Fribourg, F. Klay, and J.-F. Monin. A compared study of two correctness proofs for the standardized algorithm of abr conformance. Formal Methods in System Design, 2001. To appear."},{"key":"15_CR5","series-title":"Lect Notes Comput Sci","volume-title":"TACS\u201997","author":"S. Boutin","year":"1997","unstructured":"Samuel Boutin. Using reflection to build efficient and certified decision procedures. In Takahashi Ito and Martin Abadi, editors, TACS\u201997, volume 1281. LNCS, Springer-Verlag, 1997."},{"key":"15_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"464","DOI":"10.1007\/10722167_35","volume-title":"12th Int. Conf. Computer Aided Verification (CAV\u20192000)","author":"P. Bouyer","year":"2000","unstructured":"P. Bouyer, C. Dufourd, E. Fleury, and A. Petit. Are timed automata updatable? In 12th Int. Conf. Computer Aided Verification (CAV\u20192000), volume 1855 of Lecture Notes in Computer Science, pages 464\u2013479, Chicago, IL, USA, July 2000. Springer-Verlag."},{"key":"15_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/3-540-44612-5_19","volume-title":"25th Int. Symp. Math. Found. Comp. Sci. (MFCS\u20192000)","author":"P. Bouyer","year":"2000","unstructured":"P. Bouyer, C. Dufourd, E. Fleury, and A. Petit. Expressiveness of updatable timed automata. In 25th Int. Symp. Math. Found. Comp. Sci. (MFCS\u20192000), volume 1893 of Lecture Notes in Computer Science, pages 232\u2013242, Bratislava, Slovakia, August 2000. Springer-Verlag."},{"key":"15_CR8","unstructured":"P. Cast\u00e9ran and D. Rouillard. Reasoning about parametrized automata. In 8th International Conference on Real-Time System, 2000."},{"key":"15_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-44404-1_7","volume-title":"Logic for Programming and Automated Reasoning (LPAR\u2019 00)","author":"D. Delahaye","year":"2000","unstructured":"David Delahaye. A Tactic Language for the System coq. In Logic for Programming and Automated Reasoning (LPAR\u2019 00), volume 1955 of Lecture Notes in Computer Science, pages 85\u201395, Reunion Island, November 2000. Springer-Verlag."},{"key":"15_CR10","unstructured":"C. Paulin & E. Freund. Timed automata and the generalised abr protocol. Contribution to the Coq system, 2000. \n                    http:\/\/coq.inria.fr\n                    \n                  ."},{"key":"15_CR11","series-title":"Research Report","volume-title":"A closed-form evaluation for extended timed automata","author":"L. Fribourg","year":"1998","unstructured":"L. Fribourg. A closed-form evaluation for extended timed automata. Research Report LSV-98-2, Lab. Specification and Verification, ENS de Cachan, Cachan, France, March 1998."},{"key":"15_CR12","series-title":"Lect Notes Comput Sci","volume-title":"8th Conf on Computer-Aided Verification (CAV\u201996)","author":"S. Graf","year":"1996","unstructured":"S. Graf and H. Saidi. Verifying invariants using theorem proving. In 8th Conf on Computer-Aided Verification (CAV\u201996), volume 1102 of Lecture Notes in Computer Science, New Brunswick, NJ, USA, July 1996. Springer-Verlag."},{"key":"15_CR13","series-title":"Lect Notes Comput Sci","volume-title":"Theorem Proving in Higher Order Logics 11th International Conference (TPHOLs\u201998)","author":"E. L. Gunter","year":"1998","unstructured":"E. L. Gunter. Adding external decision procedures to hol90 securely. In Jim Grundy and Malcolm Newey, editors, Theorem Proving in Higher Order Logics 11th International Conference (TPHOLs\u201998), volume 1479 of Lecture Notes in Computer Science. Canberra, Australia, Springer-Verlag, September 1998."},{"key":"15_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/3-540-60630-0_3","volume-title":"TACAS\u201995","author":"T. Henzinger","year":"1995","unstructured":"T. Henzinger, P.-F. Ho, and H. Wong-Toi. A user guide to HYTECH. In TACAS\u201995, volume 1019 of Lecture Notes in Computer Science, pages 41\u201371, 1995."},{"key":"15_CR15","series-title":"Lect Notes Comput Sci","volume-title":"Theorem Proving in Higher-Order Logics","author":"D. Hirschkoff","year":"1997","unstructured":"D. Hirschkoff. A full formalisation of the ?-calculus theory in the Calculus of Constructions. In E. Gunter and A. Felty, editors, Theorem Proving in Higher-Order Logics, volume 1275 of Lecture Notes in Computer Science. Springer-Verlag, 1997."},{"key":"15_CR16","unstructured":"F. Honsell, M. Miculan, and I. Scagnetto. Picalculus in (co)inductive type theories. Technical report, Dipartimento di Matematica e Informatica, Universita\u2019 di Udine, 1998."},{"key":"15_CR17","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/BFb0097797","volume":"1512","author":"J.-F. Monin","year":"1998","unstructured":"J.-F. Monin. Proving a real time algorithm for ATM in Coq. In Typesfor Proofs and Programs(TYPES\u201996), volume 1512 of Lecture Notes in Computer Science, pages 277\u2013293. Springer-Verlag, 1998.","journal-title":"Typesfor Proofs and Programs(TYPES\u201996)"},{"key":"15_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"662","DOI":"10.1007\/3-540-48119-2_37","volume-title":"Formal Methods\u201999","author":"J.-F. Monin","year":"1999","unstructured":"J.-F. Monin and F. Klay. Correctness proof of the standardized algorithm for ABR conformance. In Formal Methods\u201999, volume 1708 of Lecture Notes in Computer Science, pages 662\u2013681. Springer-Verlag, 1999."},{"key":"15_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/3-540-61474-5_91","volume-title":"Computer-Aided Verification, CAV\u2019 96","author":"S. Owre","year":"1996","unstructured":"S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M.K. Srivas. PVS: Combining specification, proof checking, and model checking. In Rajeev Alur and Thomas A. Henzinger, editors, Computer-Aided Verification, CAV\u2019 96, volume 1102 of Lecture Notes in Computer Science, pages 411\u2013414, New Brunswick, NJ, July\/August 1996. Springer-Verlag."},{"key":"15_CR20","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/0304-3975(93)90222-F","volume":"116","author":"P. Z. Revesz","year":"1993","unstructured":"P. Z. Revesz. A closed-form evaluation for datalog queries with integer (gap)-order constraints. Theoretical Computer Science, 116:117\u2013149, 1993.","journal-title":"Theoretical Computer Science"},{"key":"15_CR21","series-title":"Lect Notes Comput Sci","volume-title":"12th Int. Conf. Computer Aided Verification (CAV\u201900)","author":"M. Rusinowitch","year":"2000","unstructured":"M. Rusinowitch, S. Stratulat, and F. Klay. Mechanical verification of a generic incremental ABR conformance algorithm. In 12th Int. Conf. Computer Aided Verification (CAV\u201900), volume 1855 of Lecture Notes in Computer Science, Chicago, IL, USA, July 2000. Springer-Verlag."},{"key":"15_CR22","series-title":"Lect Notes Comput Sci","volume-title":"TACAS\u201998","author":"C. Sprenger","year":"1998","unstructured":"C. Sprenger. A verified model-checker for the modal \u03bc-calculus in Coq. In TACAS\u201998, volume 1384 of Lecture Notes in Computer Science, Lisbon, Portugal, 1998. Springer-Verlag."},{"key":"15_CR23","unstructured":"The Coq Development Team. The Coq Proof Assistant Reference Manual-Version V7.0, April 2001. \n                    http:\/\/coq.inria.fr\n                    \n                  ."},{"key":"15_CR24","unstructured":"K. N. Verma. Reflecting symbolic model checking in coq. M\u2019emoire de dea, DEA Programmation, September 2000. \n                    http:\/\/www.lsv.enscachan. fr\/Publis\/PAPERS\/Ver-dea2000.ps\n                    \n                  ."},{"key":"15_CR25","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1007\/3-540-44464-5_13","volume-title":"6th Asian Computing Science Conference (ASIAN\u20192000)","author":"K. N. Verma","year":"2000","unstructured":"K. N. Verma, J. Goubault-Larrecq, S. Prasad, and S. Arun-Kumar. Reflecting bdds in coq. In 6th Asian Computing Science Conference (ASIAN\u20192000), volume 1961 of Lecture Notes in Computer Science, pages 162\u2013181. Springer-Verlag, November 2000."},{"key":"15_CR26","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"442","DOI":"10.1007\/3-540-63533-5_23","volume-title":"FME\u201997","author":"S. Yu","year":"1997","unstructured":"S. Yu and Z. Luo. Implementing a model-checker for LEGO. In J. Fitzgerald, C. B. Jones, and P. Lucas, editors, FME\u201997, volume 1313 of Lecture Notes in Computer Science, pages 442\u2013458, September 1997."}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computer Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45500-0_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,24]],"date-time":"2019-02-24T10:01:25Z","timestamp":1551002485000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45500-0_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540427360","9783540455004"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-45500-0_15","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}