{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:58:06Z","timestamp":1776333486553,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540292098","type":"print"},{"value":"9783540319696","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11562948_35","type":"book-chapter","created":{"date-parts":[[2005,10,10]],"date-time":"2005-10-10T10:06:40Z","timestamp":1128938800000},"page":"474-488","source":"Crossref","is-referenced-by-count":50,"title":["Flat Acceleration in Symbolic Model Checking"],"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"}]},{"given":"J\u00e9r\u00f4me","family":"Leroux","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Philippe","family":"Schnoebelen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"35_CR1","first-page":"39","volume":"25","author":"P.A. Abdulla","year":"2004","unstructured":"Abdulla, P.A., Collomb-Annichini, A., Bouajjani, A., Jonsson, B.: Using forward reachability analysis for verification of lossy channel systems. FMSD\u00a025(1), 39\u201365 (2004)","journal-title":"FMSD"},{"key":"35_CR2","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":"35_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)"},{"issue":"1","key":"35_CR4","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R. Alur","year":"1995","unstructured":"Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. TCS\u00a0138(1), 3\u201334 (1995)","journal-title":"TCS"},{"issue":"2","key":"35_CR5","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. TCS\u00a0126(2), 183\u2013235 (1994)","journal-title":"TCS"},{"key":"35_CR6","unstructured":"alv, www.cs.ucsb.edu\/~bultan\/composite\/"},{"key":"35_CR7","unstructured":"babylon, www.ulb.ac.be\/di\/ssd\/lvbegin\/CST\/"},{"key":"35_CR8","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":"35_CR9","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: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 576\u2013590. Springer, Heidelberg (2004)"},{"key":"35_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/978-3-540-27813-9_25","volume-title":"Computer Aided Verification","author":"C. Bartzis","year":"2004","unstructured":"Bartzis, C., Bultan, T.: Widening arithmetic automata. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 321\u2013333. Springer, Heidelberg (2004)"},{"key":"35_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/3-540-63166-6_18","volume-title":"Computer Aided Verification","author":"B. Boigelot","year":"1997","unstructured":"Boigelot, B., Bronne, L., Rassart, S.: Improved reachability analysis method for strongly linear hybrid systems. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 167\u2013178. Springer, Heidelberg (1997)"},{"key":"35_CR12","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":"5\u20136","key":"35_CR13","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1016\/S0020-0190(00)00055-7","volume":"74","author":"A. Bouajjani","year":"2000","unstructured":"Bouajjani, A., Esparza, J., Finkel, A., Maler, O., Rossmanith, P., Willems, B., Wolper, P.: An efficient automata approach to some problems on context-free grammars. IPL\u00a074(5\u20136), 221\u2013227 (2000)","journal-title":"IPL"},{"issue":"1\u20132","key":"35_CR14","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. TCS\u00a0221(1\u20132), 211\u2013250 (1999)","journal-title":"TCS"},{"key":"35_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/10722167_31","volume-title":"Computer Aided Verification","author":"A. Bouajjani","year":"2000","unstructured":"Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular Model Checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 403\u2013418. Springer, Heidelberg (2000)"},{"key":"35_CR16","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Muscholl, A., Touili, T.: Permutation rewriting and algorithmic verification. In: Proc. LICS 2001, pp. 399\u2013408 (2001)","DOI":"10.1109\/LICS.2001.932515"},{"issue":"2","key":"35_CR17","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1145\/322374.322380","volume":"30","author":"D. Brand","year":"1983","unstructured":"Brand, D., Zafiropulo, P.: On communicating finite-state machines. JACM\u00a030(2), 323\u2013342 (1983)","journal-title":"JACM"},{"key":"35_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"400","DOI":"10.1007\/3-540-63166-6_39","volume-title":"Computer Aided Verification","author":"T. Bultan","year":"1997","unstructured":"Bultan, T., Gerber, R., Pugh, W.: Symbolic model-checking of infinite state systems using Presburger arithmetic. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 400\u2013411. Springer, Heidelberg (1997)"},{"key":"35_CR19","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"35_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/BFb0028751","volume-title":"Computer Aided Verification","author":"H. Comon","year":"1998","unstructured":"Comon, H., Jurski, Y.: Multiple counters automata, safety analysis, and Presburger arithmetic. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 268\u2013279. Springer, Heidelberg (1998)"},{"key":"35_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/3-540-48320-9_18","volume-title":"CONCUR\u201999. Concurrency Theory","author":"H. Comon","year":"1999","unstructured":"Comon, H., Jurski, Y.: Timed automata and the theory of real numbers. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol.\u00a01664, pp. 242\u2013257. Springer, Heidelberg (1999)"},{"issue":"2","key":"35_CR22","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1145\/234528.234740","volume":"28","author":"P. Cousot","year":"1996","unstructured":"Cousot, P.: Abstract interpretation. ACM Comp. Surv.\u00a028(2), 324\u2013328 (1996)","journal-title":"ACM Comp. Surv."},{"key":"35_CR23","doi-asserted-by":"crossref","unstructured":"Darlot, C., Finkel, A., Van Begin, L.: About Fast and TReX accelerations. In: Proc. AVoCS 2004, ENTCS, vol.\u00a0128(6), pp. 87\u2013103 (2005)","DOI":"10.1016\/j.entcs.2005.04.006"},{"issue":"2\u20133","key":"35_CR24","first-page":"268","volume":"5","author":"G. Delzanno","year":"2004","unstructured":"Delzanno, G., Raskin, J.-F., Van Begin, L.: Covering sharing trees: a compact data structure for parameterized verification. JSTTT\u00a05(2\u20133), 268\u2013297 (2004)","journal-title":"JSTTT"},{"issue":"1","key":"35_CR25","doi-asserted-by":"crossref","first-page":"13","DOI":"10.3233\/FI-1997-3112","volume":"31","author":"J. Esparza","year":"1997","unstructured":"Esparza, J.: Petri nets, commutative context-free grammars, and basic parallel processes. Fund. Informaticae\u00a031(1), 13\u201325 (1997)","journal-title":"Fund. Informaticae"},{"key":"35_CR26","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":"35_CR27","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.: Well-abstracted transition systems: Application to FIFO automata. Inf.\u00a0&\u00a0Comp.\u00a0181(1), 1\u201331 (2003)","journal-title":"Inf.\u00a0&\u00a0Comp."},{"issue":"1\u20132","key":"35_CR28","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","volume":"256","author":"A. Finkel","year":"2001","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! TCS\u00a0256(1\u20132), 63\u201392 (2001)","journal-title":"TCS"},{"key":"35_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1007\/3-540-63141-0_15","volume-title":"CONCUR\u201997: Concurrency Theory","author":"L. Fribourg","year":"1997","unstructured":"Fribourg, L., Ols\u00e9n, H.: Proving Safety Properties of Infinite State Systems by Compilation into Presburger Arithmetic. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol.\u00a01243, pp. 213\u2013227. Springer, Heidelberg (1997)"},{"key":"35_CR30","unstructured":"Fribourg, L.: Petri nets, flat languages and linear arithmetic. In: Alpuente, M. (ed.) Proc. WFLP 2000, pp. 344\u2013365 (2000)"},{"issue":"1","key":"35_CR31","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0304-3975(01)00268-7","volume":"289","author":"O.H. Ibarra","year":"2002","unstructured":"Ibarra, O.H., Su, J., Dang, Z., Bultan, T., Kemmerer, R.A.: Counter machines and verification problems. TCS\u00a0289(1), 165\u2013189 (2002)","journal-title":"TCS"},{"issue":"1\u20132","key":"35_CR32","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/S0304-3975(00)00103-1","volume":"256","author":"Y. Kesten","year":"2001","unstructured":"Kesten, Y., Maler, O., Marcus, M., Pnueli, A., Shahar, E.: Symbolic model checking with rich assertional languages. TCS\u00a0256(1\u20132), 93\u2013112 (2001)","journal-title":"TCS"},{"key":"35_CR33","unstructured":"lash, www.montefiore.ulg.ac.be\/~boigelot\/research\/lash\/"},{"key":"35_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1007\/978-3-540-28644-8_26","volume-title":"CONCUR 2004 - Concurrency Theory","author":"J. Leroux","year":"2004","unstructured":"Leroux, J., Sutre, G.: On flatness for 2-dimensional vector addition systems with states. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 402\u2013416. Springer, Heidelberg (2004)"},{"key":"35_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/11562948_36","volume-title":"Automated Technology for Verification and Analysis","author":"J. Leroux","year":"2005","unstructured":"Leroux, J., Sutre, G.: Flat counter automata almost everywhere! In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol.\u00a03707, pp. 489\u2013503. Springer, Heidelberg (2005)"},{"key":"35_CR36","unstructured":"Pachl, J.K.: Protocol description and analysis based on a state transition model with channel expressions. In: Proc. PSTV 1987, pp. 207\u2013219 (1987)"},{"key":"35_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/3-540-45719-4_33","volume-title":"Algebraic Methodology and Software Technology","author":"T. Rybina","year":"2002","unstructured":"Rybina, T., Voronkov, A.: Brain: Backward reachability analysis with integers. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol.\u00a02422, pp. 489\u2013494. Springer, Heidelberg (2002)"},{"key":"35_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/BFb0028736","volume-title":"Computer Aided Verification","author":"P. Wolper","year":"1998","unstructured":"Wolper, P., Boigelot, B.: Verifying systems with infinite but regular state spaces. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 88\u201397. Springer, Heidelberg (1998)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11562948_35.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T14:52:20Z","timestamp":1605624740000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11562948_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540292098","9783540319696"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/11562948_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}