{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:16:06Z","timestamp":1725574566678},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540236108"},{"type":"electronic","value":"9783540304760"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-30476-0_22","type":"book-chapter","created":{"date-parts":[[2011,1,12]],"date-time":"2011-01-12T12:51:35Z","timestamp":1294836695000},"page":"248-262","source":"Crossref","is-referenced-by-count":1,"title":["Composition of Accelerations to Verify Infinite Heterogeneous Systems"],"prefix":"10.1007","author":[{"given":"S\u00e9bastien","family":"Bardin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alain","family":"Finkel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"22_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/10722167_32","volume-title":"Computer Aided Verification","author":"A. Annichini","year":"2000","unstructured":"Annichini, A., Asarin, E., Bouajjani, A.: Symbolic techniques for parametric reasoning about counter and clock systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 419\u2013434. Springer, Heidelberg (2000)"},{"key":"22_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/BFb0028754","volume-title":"Computer Aided Verification","author":"P.A. Abdulla","year":"1998","unstructured":"Abdulla, P.A., Bouajjani, A., Jonsson, B.: On-thefly analysis of systems with unbounded, lossy FIFO channels. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 305\u2013318. Springer, Heidelberg (1998)"},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/3-540-44585-4_34","volume-title":"Computer Aided Verification","author":"A. Annichini","year":"2001","unstructured":"Annichini, A., Bouajjani, A., Sighireanu, M.: TReX: a Tool for Reachability analysis of Complex Systems. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 368\u2013372. Springer, Heidelberg (2001)"},{"key":"22_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1007\/3-540-61064-2_27","volume-title":"Trees in Algebra and Programming - CAAP \u201996","author":"A. Boudet","year":"1996","unstructured":"Boudet, A., Comon, H.: Diophantine equations, Presburger arithmetic and finite automata. In: Kirchner, H. (ed.) CAAP 1996. LNCS, vol.\u00a01059, pp. 30\u201343. Springer, Heidelberg (1996)"},{"key":"22_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1007\/978-3-540-24730-2_42","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Bardin","year":"2004","unstructured":"Bardin, S., Finkel, A., Leroux, J.: FASTer acceleration of counter automata in practice. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 576\u2013590. Springer, Heidelberg (2004)"},{"key":"22_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-540-45069-6_12","volume-title":"Computer Aided Verification","author":"S. Bardin","year":"2003","unstructured":"Bardin, S., Finkel, A., Leroux, J., Petrucci, L.: FAST: Fast Acceleration of Symbolic Transition systems. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 118\u2013121. Springer, Heidelberg (2003)"},{"key":"22_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/BFb0032741","volume-title":"Static Analysis","author":"B. Boigelot","year":"1997","unstructured":"Boigelot, B., Godefroid, P., Willems, B., Wolper, P.: The power of QDDs. In: Van Hentenryck, P. (ed.) SAS 1997. LNCS, vol.\u00a01302, pp. 172\u2013186. Springer, Heidelberg (1997)"},{"issue":"1-2","key":"22_CR8","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1016\/S0304-3975(99)00033-X","volume":"221","author":"A. Bouajjani","year":"1999","unstructured":"Bouajjani, A., Habermehl, P.: Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations. Theoretical Computer Science\u00a0221(1-2), 211\u2013250 (1999)","journal-title":"Theoretical Computer Science"},{"key":"22_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-540-45069-6_19","volume-title":"Computer Aided Verification","author":"B. Boigelot","year":"2003","unstructured":"Boigelot, B., Herbreteau, F., Jodogne, S.: Hybrid acceleration using real vector automata. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 193\u2013205. Springer, Heidelberg (2003)"},{"key":"22_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"588","DOI":"10.1007\/3-540-45744-5_50","volume-title":"Automated Reasoning","author":"B. Boigelot","year":"2001","unstructured":"Boigelot, B., Jodogne, S., Wolper, P.: On the use of weak automata for deciding linear arithmetic with integer and real variables. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 588\u2013603. Springer, Heidelberg (2001)"},{"key":"22_CR11","unstructured":"Boigelot, B.: Symbolic Methods for Exploring Infinite State Spaces. PhD thesis, Universit\u00e9 de Li\u00e8ge (1998)"},{"key":"22_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/3-540-48224-5_3","volume-title":"Automata, Languages and Programming","author":"A. Bouajjani","year":"2001","unstructured":"Bouajjani, A.: Languages, rewriting systems, and verification of infinite-state systems. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol.\u00a02076, pp. 24\u201339. Springer, Heidelberg (2001)"},{"issue":"3","key":"22_CR13","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R.E. Bryant","year":"1992","unstructured":"Bryant, R.E.: Symbolic boolean manipulation with ordered binarydecision diagrams. ACM Computing Surveys\u00a024(3), 293\u2013318 (1992)","journal-title":"ACM Computing Surveys"},{"key":"22_CR14","first-page":"238","volume-title":"Proc. 4th ACM Symp. Principles of Programming Languages","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. 4th ACM Symp. Principles of Programming Languages, Los Angeles, CA, USA, January 1977, pp. 238\u2013253. ACM, New York (1977)"},{"key":"22_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/3-540-52148-8_17","volume-title":"Automatic Verification Methods for Finite State Systems","author":"D.L. Dill","year":"1990","unstructured":"Dill, D.L.: Timing assumption and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol.\u00a0407, pp. 197\u2013212. Springer, Heidelberg (1990)"},{"key":"22_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/3-540-36206-1_14","volume-title":"FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science","author":"A. Finkel","year":"2002","unstructured":"Finkel, A., Leroux, J.: How to compose Presburger-accelerations: Applications to broadcast protocols. In: Agrawal, M., Seth, A.K. (eds.) FSTTCS 2002. LNCS, vol.\u00a02556, pp. 145\u2013156. Springer, Heidelberg (2002)"},{"issue":"1","key":"22_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0890-5401(02)00027-5","volume":"181","author":"A. Finkel","year":"2003","unstructured":"Finkel, A., Purushothaman Iyer, S., Sutre, G.: Wellabstracted transition systems: Application to FIFO automata. Information and Computation\u00a0181(1), 1\u201331 (2003)","journal-title":"Information and Computation"},{"issue":"2","key":"22_CR18","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1023\/A:1008678014487","volume":"11","author":"N. Halbwachs","year":"1997","unstructured":"Halbwachs, N., Proy, Y.E., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Formal Methods in System Design\u00a011(2), 157\u2013185 (1997)","journal-title":"Formal Methods in System Design"},{"key":"22_CR19","unstructured":"lash homepage, http:\/\/www.montefiore.ulg.ac.be\/~boigelot\/research\/lash\/"},{"key":"22_CR20","series-title":"Electronic Notes in Theor. Comp. Sci","volume-title":"Proc. 5th Int. Workshop on Verification of Infinite State Systems (INFINITY 2003)","author":"J. Leroux","year":"2003","unstructured":"Leroux, J.: The affine hull of a binary automaton is computable in polynomial time. In: Proc. 5th Int. Workshop on Verification of Infinite State Systems (INFINITY 2003), Marseille, France, September 2003. Electronic Notes in Theor. Comp. Sci, Elsevier Science, Amsterdam (2003)"},{"key":"22_CR21","doi-asserted-by":"crossref","unstructured":"Tavernier, B.: Calife: a generic graphical user interface for automota tools. In: Proc. of the 4th Workshop on Language Descriptions, Tools and Applications (LDTA 2004), Barcelona, Spain (April 2004)","DOI":"10.1016\/j.entcs.2004.06.004"},{"key":"22_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-46419-0_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P. Wolper","year":"2000","unstructured":"Wolper, P., Boigelot, B.: On the construction of automata from linear arithmetic constraints. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol.\u00a01785, pp. 1\u201319. Springer, Heidelberg (2000)"},{"key":"22_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/3-540-45319-9_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Yavuz-Kahveci","year":"2001","unstructured":"Yavuz-Kahveci, T., Tuncer, M., Bultan, T.: A library for composite symbolic representations. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 52\u201366. Springer, Heidelberg (2001)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-30476-0_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,17]],"date-time":"2021-11-17T01:37:58Z","timestamp":1637113078000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-30476-0_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540236108","9783540304760"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-30476-0_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}