{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:33:05Z","timestamp":1754483585100},"publisher-location":"Berlin, Heidelberg","reference-count":9,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540651376"},{"type":"electronic","value":"9783540495628"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0097797","type":"book-chapter","created":{"date-parts":[[2006,11,24]],"date-time":"2006-11-24T14:27:48Z","timestamp":1164378468000},"page":"277-293","source":"Crossref","is-referenced-by-count":7,"title":["Proving a real time algorithm for ATM in Coq"],"prefix":"10.1007","author":[{"given":"Jean-Fran\u00e7ois","family":"Monin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,10,26]]},"reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"R. Alur C. Courcoubetis and D. Dill. Model-Checking for Real-Time Systems. In 5th Symp. on Logic in Compouter Science. IEEE, 1990.","DOI":"10.1007\/3-540-54233-7_128"},{"key":"15_CR2","volume-title":"Parallel Program Design","author":"K. M. Chandy","year":"1989","unstructured":"K. M. Chandy and J. Misra. Parallel Program Design. Austin, Texas, Addison-Wesley, 1989."},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"D. Clark, E. M. Emerson eand A. P. Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications: a practical approach. Proc. 10th ACM Symp. on Principles of Programming Languages. 1983.","DOI":"10.1145\/567067.567080"},{"key":"15_CR4","unstructured":"B. Barras, S. Boutin, C. Cornes, J. Courant, J-C. Filli\u00e2tre, E. Gim\u00e9nez, H. Herbelin, G. Huet, P. Manoury, C. Mu\u00f1oz, C. Murthy, C. Parent, C. Paulin-Mohring, A. Saibi and B. Werner, The Coq Proof Assistant User's Guide, version 6.1 (INRIA-Rocquencourt et CNRS-ENS Lyon, November 1996)"},{"key":"15_CR5","unstructured":"ITU-T Recommendation I.361.1 Traffic control and congestion control in B-ISDN, February 1997"},{"key":"15_CR6","unstructured":"E. Harel O. Lichtenstein and A. Pnueli. Explicit clock temporal logic. In 5th Symp. on Logic in Compouter Science. IEEE, 1990."},{"key":"15_CR7","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"T. A. Henzinger","year":"1994","unstructured":"Thomas A. Henzinger, Xavier Nicollin, Joseph Sifakis, and Sergio Yovine. Symbolic Model Checking for Real-Time Systems, Information and Computation, 111 (1994) 193\u2013244","journal-title":"Information and Computation"},{"key":"15_CR8","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16\u20133","author":"L. Lamport","year":"1994","unstructured":"L. Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16\u20133 (1994), 872\u2013923.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"15_CR9","unstructured":"Jean-Fran\u00e7ois Monin and Francis Klay Formal specification and correction of I.371.1 algorithm for ABR conformance, internal report NT DTL\/MSV\/003, CNET. 1997"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0097797","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,22]],"date-time":"2019-04-22T14:53:44Z","timestamp":1555944824000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0097797"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540651376","9783540495628"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/bfb0097797","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}