{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:58:17Z","timestamp":1754488697854},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540423454"},{"type":"electronic","value":"9783540445852"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44585-4_34","type":"book-chapter","created":{"date-parts":[[2010,2,11]],"date-time":"2010-02-11T19:39:50Z","timestamp":1265917190000},"page":"368-372","source":"Crossref","is-referenced-by-count":45,"title":["TReX: A Tool for Reachability Analysis of Complex Systems"],"prefix":"10.1007","author":[{"given":"Aurore","family":"Annichini","sequence":"first","affiliation":[]},{"given":"Ahmed","family":"Bouajjani","sequence":"additional","affiliation":[]},{"given":"Mihaela","family":"Sighireanu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,7,4]]},"reference":[{"key":"34_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1007\/BFb0028754","volume-title":"Proceedings of the 10th CAV","author":"P.A. Abdulla","year":"1998","unstructured":"P.A. Abdulla, A. Bouajjani, and B. Jonsson. On-the-fly analysis of systems with unbounded, lossy, FIFO channels. In Proceedings of the 10th CAV, volume 1427 of LNCS, pages 305\u2013317. Springer Verlag, 1998."},{"key":"34_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"419","DOI":"10.1007\/10722167_32","volume-title":"Proceedings of the 12th CAV","author":"A. Annichini","year":"2000","unstructured":"A. Annichini, E. Asarin, and A. Bouajjani. Symbolic techniques for parametric reasoning about counter and clock systems. In E.A. Emerson and A.P. Sistla, editors, Proceedings of the 12th CAV, volume 1855 of LNCS, pages 419\u2013434. Springer Verlag, July 2000."},{"key":"34_CR3","series-title":"Lect Notes Comput Sci","volume-title":"Proceedings of the 10th CAV","author":"S. Bensalem","year":"1998","unstructured":"S. Bensalem, Y. Lakhnech, and S. Owre. InVeSt: A tool for the verification of invariants. In Proceedings of the 10th CAV, volume 1427 of LNCS. Springer Verlag, 1998."},{"key":"34_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1007\/10722167_31","volume-title":"Proceedings of the 12th CAV","author":"A. Bouajjani","year":"2000","unstructured":"A. Bouajjani, B. Jonsson, M. Nilsson, and T. Touili. Regular model checking. In E.A. Emerson and A.P. Sistla, editors, Proceedings of the 12th CAV, volume 1855 of LNCS, pages 403\u2013418, July 2000."},{"key":"34_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"543","DOI":"10.1007\/10722167_41","volume-title":"Proceedings of the 12th CAV","author":"M. Bozga","year":"2000","unstructured":"M. Bozga, J.-C. Fernandez, L. Girvu, S. Graf, J.-P. Krimm, and L. Mounier. If: A validation environment for times asynchronous systems. In E.A. Emerson and A.P. Sistla, editors, Proceedings of the 12th CAV, volume 1855 of LNCS, pages 543\u2013547. Springer Verlag, July 2000."},{"key":"34_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1007\/BFb0035403","volume-title":"Proceedings of 3rd Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"P.R. DArgenio","year":"1997","unstructured":"P.R. D\u2019Argenio, J.-P. Katoen, T.C. Ruys, and J. Tretmans. The bounded retransmission protocol must be on time! In Proceedings of 3rd Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 1217 of LNCS, pages 416\u2013432. Springer Verlag, 1997."},{"key":"34_CR7","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/BF01585709","volume":"53","author":"B.C. Eaves","year":"1992","unstructured":"B.C. Eaves and U.G. Rothblum. Dines-fourier-motzkin quantifier elimination and an application of corresponding transfer principles over ordered fields. Mathematical Programming, 53:307\u2013321, 1992.","journal-title":"Mathematical Programming"},{"key":"34_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"437","DOI":"10.1007\/3-540-61474-5_97","volume-title":"Proceedings of the 8th CAV","author":"J.-C. Fernandez","year":"1996","unstructured":"J.-C. Fernandez, H. Garavel, A. Kerbrat, R. Mateescu, L. Mounier, and M. Sighireanu. Cadp (c\u00e6sar\/aldebaran development package): A protocol validation and verification toolbox. In R. Alur and T.A. Henzinger, editors, Proceedings of the 8th CAV, volume 1102 of LNCS, pages 437\u2013440. Springer Verlag, August 1996."},{"key":"34_CR9","unstructured":"A.C. Hearn. REDUCE \u2014 User\u2019s and Contributed Packages Manual. Codemist Ltd., February 1999. version 3.7."},{"issue":"1","key":"34_CR10","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"T.A. Henzinger","year":"1997","unstructured":"T.A. Henzinger, P.-H. Ho, and H. Wong-Toi. Hytech: A model checker for hybrid systems. Software Tools for Technology Transfer, 1(1):110\u2013122, 1997.","journal-title":"Software Tools for Technology Transfer"},{"key":"34_CR11","unstructured":"G.J. Holzmann. Design and Validation of Computer Protocols. Software Series. Prentice Hall, 1991."},{"key":"34_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1007\/BFb0055344","volume-title":"Proceedings of 5th FTRTFT","author":"R.F. Lutje Spelberg","year":"1998","unstructured":"R.F. Lutje Spelberg, W.J. Toetenel, and M. Ammerlaan. Partion refinement in real-time model checking. In A.P. Ravn and H. Rischel, editors, Proceedings of 5th FTRTFT, volume 1486 of LNCS, pages 143\u2013157. Springer Verlag, 1998."},{"key":"34_CR13","unstructured":"K.L. McMillan. The SMV system. Cadence Berkeley Labs, 1999."},{"key":"34_CR14","unstructured":"Omega Team. The Omega Library, November 1996. version 1.1.0."},{"key":"34_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46419-0_1","volume-title":"Proceedings of the 6th Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Wolper","year":"2000","unstructured":"P. Wolper and B. Boigelot. On the construction of automata from linear arithmetic constraints. In S. Graf and M. Schwartzbach, editors, Proceedings of the 6th Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 1785 of LNCS. Springer Verlag, 2000."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44585-4_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,23]],"date-time":"2019-02-23T19:15:08Z","timestamp":1550949308000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44585-4_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540423454","9783540445852"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-44585-4_34","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}