{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,26]],"date-time":"2025-09-26T13:07:52Z","timestamp":1758892072656},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540677703"},{"type":"electronic","value":"9783540450474"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10722167_41","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T22:00:33Z","timestamp":1167429633000},"page":"543-547","source":"Crossref","is-referenced-by-count":16,"title":["IF: A Validation Environment for Timed Asynchronous Systems"],"prefix":"10.1007","author":[{"given":"Marius","family":"Bozga","sequence":"first","affiliation":[]},{"given":"Jean-Claude","family":"Fernandez","sequence":"additional","affiliation":[]},{"given":"Lucian","family":"Ghirvu","sequence":"additional","affiliation":[]},{"given":"Susanne","family":"Graf","sequence":"additional","affiliation":[]},{"given":"Jean-Pierre","family":"Krimm","sequence":"additional","affiliation":[]},{"given":"Laurent","family":"Mounier","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"41_CR1","unstructured":"Telelogic AB. SDT Reference Manual, http:\/\/www.telelogic.se"},{"key":"41_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BFb0028755","volume-title":"Computer Aided Verification","author":"S. Bensalem","year":"1998","unstructured":"Bensalem, S., Lakhnech, Y., Owre, S.: Computing Abstractions of Infinite State Systems Compositionally and Automatically. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 319\u2013331. Springer, Heidelberg (1998)"},{"key":"41_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-49213-5_5","volume-title":"Compositionality: The Significant Difference","author":"S. Bornot","year":"1998","unstructured":"Bornot, S., Sifakis, J., Tripakis, S.: Modeling urgency in timed systems. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol.\u00a01536, p. 103. Springer, Heidelberg (1998)"},{"key":"41_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/3-540-46419-0_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Bo\u0161na\u010dki","year":"2000","unstructured":"Bo\u0161na\u010dki, D., Dams, D.R., Holenderski, L., Sidorova, N.: Model checking SDL with spin. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol.\u00a01785, pp. 363\u2013377. Springer, Heidelberg (2000)"},{"key":"41_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/3-540-48294-6_11","volume-title":"Static Analysis","author":"M. Bozga","year":"1999","unstructured":"Bozga, M., Fernandez, J.C., Ghirvu, L.: State space reduction based on live variables analysis. In: Cortesi, A., Fil\u00e9, G. (eds.) SAS 1999. LNCS, vol.\u00a01694, pp. 164\u2013178. Springer, Heidelberg (1999)"},{"key":"41_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/3-540-46419-0_17","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Bozga","year":"2000","unstructured":"Bozga, M., Fernandez, J.C., Ghirvu, L.: Using static analysis to improve automatic test generation. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol.\u00a01785, pp. 235\u2013250. Springer, Heidelberg (2000)"},{"key":"41_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1007\/3-540-48119-2_19","volume-title":"FM\u201999 - Formal Methods","author":"M. Bozga","year":"1999","unstructured":"Bozga, M., Fernandez, J.C., Ghirvu, L., Graf, S., Krimm, J.P., Mounier, L.: IF: An Intermediate Representation and Validation Environment for Timed Asynchronous Systems. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol.\u00a01708, pp. 307\u2013327. Springer, Heidelberg (1999)"},{"issue":"1","key":"41_CR8","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/S0167-6423(99)00017-9","volume":"36","author":"M. Bozga","year":"2000","unstructured":"Bozga, M., Fernandez, J.C., Ghirvu, L., Jard, C., J\u00e9ron, T., Kerbrat, A., Morel, P., Mounier, L.: Verification and Test Generation for the SSCOP Protocol. Journal of Science of Computer Programming, Special Isssue on Formal Methods in Industry\u00a036(1), 27\u201352 (2000)","journal-title":"Journal of Science of Computer Programming, Special Isssue on Formal Methods in Industry"},{"key":"41_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"437","DOI":"10.1007\/3-540-61474-5_97","volume-title":"Computer Aided Verification","author":"J.C. Fernandez","year":"1996","unstructured":"Fernandez, J.C., Garavel, H., Kerbrat, A., Mateescu, R., Mounier, L., Sighireanu, M.: CADP: A Protocol Validation and Verification Toolbox. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 437\u2013440. Springer, Heidelberg (1996)"},{"key":"41_CR10","doi-asserted-by":"crossref","unstructured":"Fernandez, J.C., Jard, C., J\u00e9ron, T., Viho, C.: An Experiment in Automatic Generation of Test Suites for Protocols with Verification Technology. Science of Computer Programming\u00a029 (1997)","DOI":"10.1016\/S0167-6423(96)00032-9"},{"key":"41_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/BFb0054165","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Garavel","year":"1998","unstructured":"Garavel, H.: OPEN\/CAESAR: An open software architecture for verification, simulation, and testing. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, pp. 68\u201384. Springer, Heidelberg (1998)"},{"key":"41_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"460","DOI":"10.1007\/3-540-63166-6_48","volume-title":"Computer Aided Verification","author":"T.H. Henzinger","year":"1997","unstructured":"Henzinger, T.H., Ho, P.-H., Wong-Toi, H.: HyTech: A Model Checker for Hybrid Systems. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 460\u2013463. Springer, Heidelberg (1997)"},{"key":"41_CR13","unstructured":"Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice Hall Software Series (1991)"},{"key":"41_CR14","unstructured":"I-Logix. StateMate, http:\/\/www.ilogix.com\/"},{"key":"41_CR15","unstructured":"ISO\/IEC. LOTOS - A Formal Description Technique Based on the Temporal Or- dering of Observational Behaviour. Technical Report 8807, ISO\/OSI (1988)"},{"key":"41_CR16","unstructured":"ITU-T. Recommendation Z.100. Specification and Description Language (SDL). Technical Report Z-100, International Telecommunication Union - Standardization Sector, Gen\u00e8ve (1994)"},{"key":"41_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/3-540-46419-0_19","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.P. Krimm","year":"2000","unstructured":"Krimm, J.P., Mounier, L.: Compositional State Space Generation with Partial Order Reductions for Asynchronous Communicating Systems. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol.\u00a01785, pp. 266\u2013282. Springer, Heidelberg (2000)"},{"key":"41_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"456","DOI":"10.1007\/3-540-63166-6_47","volume-title":"Computer Aided Verification","author":"K.G. Larsen","year":"1997","unstructured":"Larsen, K.G., Petterson, P., Yi, W.: UPPAAL: Status & Developments. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 456\u2013459. Springer, Heidelberg (1997)"},{"key":"41_CR19","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking: an Approach to the State Explosion Problem","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking: an Approach to the State Explosion Problem. Kluwer Academic Publisher, Dordrecht (1993)"},{"key":"41_CR20","unstructured":"Verilog. ObjectGEODE Reference Manual, http:\/\/www.verilogusa.com\/"},{"key":"41_CR21","doi-asserted-by":"crossref","unstructured":"Weiser, M.: Program Slicing. IEEE Transactions on Software Engineering\u00a0SE-10(4) (July 1984)","DOI":"10.1109\/TSE.1984.5010248"},{"issue":"1+2","key":"41_CR22","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s100090050009","volume":"1","author":"S. Yovine","year":"1997","unstructured":"Yovine, S.: KRONOS: A Verification Tool for Real-Time Systems. Software Tools for Technology Transfer\u00a01(1+2), 123\u2013133 (1997)","journal-title":"Software Tools for Technology Transfer"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10722167_41","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,23]],"date-time":"2019-04-23T07:49:11Z","timestamp":1556005751000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10722167_41"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540677703","9783540450474"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/10722167_41","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}