{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:10:02Z","timestamp":1749125402788,"version":"3.41.0"},"reference-count":19,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2003,2,1]],"date-time":"2003-02-01T00:00:00Z","timestamp":1044057600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,2,1]],"date-time":"2003-02-01T00:00:00Z","timestamp":1044057600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[2003,2]]},"DOI":"10.1023\/a:1023251327012","type":"journal-article","created":{"date-parts":[[2003,6,6]],"date-time":"2003-06-06T17:39:54Z","timestamp":1054921194000},"page":"153-177","source":"Crossref","is-referenced-by-count":10,"title":["Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm"],"prefix":"10.1007","volume":"30","author":[{"given":"Micha\u00ebl","family":"Rusinowitch","sequence":"first","affiliation":[]},{"given":"Sorin","family":"Stratulat","sequence":"additional","affiliation":[]},{"given":"Francis","family":"Klay","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5112135_CR1","doi-asserted-by":"crossref","unstructured":"Arnold, A.: MEC: A system for constructing and analysing transition systems, in J. Sifakis (ed.), Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems, Lecture Notes in Comput. Sci. 407, Springer-Verlag, 1990, pp. 117-132.","DOI":"10.1007\/3-540-52148-8_11"},{"key":"5112135_CR2","unstructured":"Barras, B., Boutin, S., Cornes, C., Courant, J., Filliatre, J. C., Gim\u00e9nez, E., Herbelin, H., Huet, G., Mu\u00f1oz, C., Murthy, C., Parent, C., Paulin, C., Sa\u00efbi, A. and Werner, B.: The Coq proof assistant reference manual - version V6.1, Technical Report 0203, INRIA, August 1997."},{"key":"5112135_CR3","doi-asserted-by":"crossref","unstructured":"Bengtsson, J., Larsen, K. G., Larsson, F., Pettersson, P. and Yi, W.: UPPAAL: A tool suite for the automatic verification of real-time systems, in R. Alur, T. A. Henzinger and E. D. Sontag (eds), Hybrid Systems III, Lecture Notes in Comput. Sci. 1066, 1996, pp. 232-243.","DOI":"10.1007\/BFb0020949"},{"key":"5112135_CR4","unstructured":"Berger, A., Bonomi, F. and Fendick, K.: Proposed TM baseline text on an ABR conformance definition, Technical Report 95-0212R1, ATM Forum Traffic Management Group, 1995."},{"key":"5112135_CR5","unstructured":"Bouhoula, A. and Rusinowitch, M.: SPIKE-User Manual, December 1995."},{"key":"5112135_CR6","doi-asserted-by":"crossref","unstructured":"B\u00e9rard, B. and Fribourg, L.: Automated verification of a parametric real-time program: The ABR conformance protocol, in Proc. 11th Int. Conf. Computer Aided Verification (CAV\u201999), Lecture Notes in Comput. Sci. 1633, July 1999, pp. 96-107.","DOI":"10.1007\/3-540-48683-6_11"},{"key":"5112135_CR7","volume-title":"A Discipline of Programming","author":"E. W. Dijkstra","year":"1976","unstructured":"Dijkstra, E. W.: A Discipline of Programming, Prentice-Hall, Englewood Cliffs, 1976."},{"key":"5112135_CR8","unstructured":"Fribourg, L.: A closed-form evaluation for extended timed automata, Technical Report LSV-98-2, Lab. Specification and Verification, ENS de Cachan, March 1998. 17 pages."},{"key":"5112135_CR9","doi-asserted-by":"crossref","unstructured":"Henzinger, T. A., Ho, P. H. and Wong-Toi, H.: HYTECH: A model checker for hybrid systems, in CAV\u201997, Lecture Notes in Comput. Sci. 1254, Springer-Verlag, 1997, pp. 460-463.","DOI":"10.1007\/3-540-63166-6_48"},{"key":"5112135_CR10","doi-asserted-by":"publisher","first-page":"1723","DOI":"10.1016\/0169-7552(96)00012-8","volume":"28","author":"R. Jain","year":"1996","unstructured":"Jain, R.: Congestion control and traffic management in ATM networks: Recent advances and a survey, Computer Networks and ISDN Systems\n28 (1996), 1723-1738. ftp:\/\/ftp.netlab.ohio-state.edu\/pub\/jain\/papers\/cnis\/index.html.","journal-title":"Computer Networks and ISDN Systems"},{"key":"5112135_CR11","doi-asserted-by":"crossref","unstructured":"Monin, J. F. and Klay, F.: Correctness proof of the standardized algorithm for ABR conformance, in J. Wing, J. Woodcock and J. Davies (eds), Formal Methods (FM)\u2019 99, Lecture Notes in Comput. Sci. 1709, Springer-Verlag, 1999, pp. 662-681.","DOI":"10.1007\/3-540-48119-2_37"},{"key":"5112135_CR12","unstructured":"Owre, S. and Shankar, N.: PVS semantics document, March 1999. http:\/\/www.csl.sri.com\/papers\/csl-97-2\/"},{"key":"5112135_CR13","unstructured":"Rabadan, C.: L\u2019ABR et sa conformit\u00e9, Technical Report NT DAC\/ARP\/034, CNET, 1997."},{"key":"5112135_CR14","unstructured":"Rabadan, C. and Klay, F.: Un nouvel algorithme de contr\u00f4le de conformit\u00e9 pour la capacit\u00e9 de transfert \u201cAvailable Bit Rate\u201d, Technical Report NT\/CNET\/5476, CNET, 1997."},{"key":"5112135_CR15","doi-asserted-by":"crossref","unstructured":"Rusinowitch, M., Stratulat, S. and Klay, F.: Mechanical verification of an ideal incremental ABR conformance algorithm, in E. A. Emerson and A. P. Sistla (eds), Proceedings of 12th International Conference on Computer Aided Verification (CAV\u20192000), Lecture Notes in Comput. Sci. 1855, Springer-Verlag, July 2000, pp. 344-357.","DOI":"10.1007\/10722167_27"},{"key":"5112135_CR16","unstructured":"Shankar, N., Owre, S., Rushby, J. M. and Stringer-Calvert, D. W. J.: PVS: Prover Guide. Version 2.3, 1999."},{"issue":"9","key":"5112135_CR17","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1109\/32.713327","volume":"24","author":"J. Rushby","year":"1998","unstructured":"Rushby, J., Owre, S. and Shankar, N.: Subtypes for specifications: Predicate subtyping in PVS, IEEE Trans. on Software Engrg. 24(9) (1998), 709-720.","journal-title":"IEEE Trans. on Software Engrg."},{"key":"5112135_CR18","doi-asserted-by":"crossref","unstructured":"Shankar, N. and Owre, S.: Principles and pragmatics of subtyping in PVS, in D. Bert, C. Choppy and P. Mosses (eds), Recent Trends in Algebraic Development Techniques, WADT\u201999, Lecture Notes in Comput. Sci. 1827, Toulouse, France, September 1999, pp. 37-52.","DOI":"10.1007\/978-3-540-44616-3_3"},{"key":"5112135_CR19","unstructured":"Stratulat, S.: Preuves par r\u00e9currence avec ensembles couvrants contextuels: Applications \u00e0 la v\u00e9rification de logiciels de t\u00e9l\u00e9communications. Ph.D. thesis, Universit\u00e9 Henri Poincar\u00e9, Nancy I, 2000."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1023251327012.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1023251327012\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1023251327012.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:33:28Z","timestamp":1749123208000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1023251327012"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,2]]},"references-count":19,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2003,2]]}},"alternative-id":["5112135"],"URL":"https:\/\/doi.org\/10.1023\/a:1023251327012","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2003,2]]}}}