{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T01:40:18Z","timestamp":1737078018769,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540433811"},{"type":"electronic","value":"9783540459880"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45988-x_7","type":"book-chapter","created":{"date-parts":[[2007,6,7]],"date-time":"2007-06-07T02:19:02Z","timestamp":1181182742000},"page":"72-86","source":"Crossref","is-referenced-by-count":2,"title":["Constraint-Based Model Checking for Parameterized Synchronous Systems"],"prefix":"10.1007","author":[{"given":"Giorgio","family":"Delzanno","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,3,14]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"P. A. Abdulla, K. Cer\u0101ns, B. Jonsson and Y.-K. Tsay. General Decidability Theorems for Infinite-State Systems. In Proc. of LICS 96, pp. 313\u2013321, 1996.","DOI":"10.1109\/LICS.1996.561359"},{"key":"7_CR2","unstructured":"M. Ajmone Marsan, G. Balbo, G. Conte, S. Donatelli, and G. Franceschinis. Modelling with Generalized Stochastic Petri Nets. Series in Parallel Computing. John Wiley & Sons, 1995."},{"key":"7_CR3","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"15","author":"K. Apt","year":"1986","unstructured":"K. Apt and D. Kozen. Limits for Automatic Verification of Finite-state Concurrent Systems. Information Processing Letters 15, pp. 307\u2013309, 1986.","journal-title":"Information Processing Letters"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"T. Ball, S. Chaki, S. K. Rajamani. Parameterized Verification of Multithreaded Software Libraries. In Proc. TACAS\u2019 01, LNAI 2031, pages 158\u2013173, 2001.","DOI":"10.1007\/3-540-45319-9_12"},{"issue":"1","key":"7_CR5","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1016\/0890-5401(89)90026-6","volume":"81","author":"M. C. Browne","year":"1989","unstructured":"M. C. Browne, E. M. Clarke, O. Grumberg. Reasoning about Networks with Many Identical Finite State Processes. Information and Computation 81(1): 13\u201331, 1989.","journal-title":"Information and Computation"},{"key":"7_CR6","doi-asserted-by":"crossref","unstructured":"B. B\u00e9rard, and L. Fribourg. Reachability analysis of (timed) Petri nets using real arithmetic. In Proc. of CONCUR 99, LNAI 1664, pp. 178\u2013193.","DOI":"10.1007\/3-540-48320-9_14"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"B. Boigelot and P. Wolper. Verifying Systems with Infinite but Regular State Space. In Proc. of CAV 98, LNAI 1427, pp. 88\u201397. Springer, 1998.","DOI":"10.1007\/BFb0028736"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"A. Bouajjani and R. Mayr. Model Checking Lossy Vector Addition Systems. In Proc. of STACS 99, LNAI 1563, pp. 323\u2013333. 1999.","DOI":"10.1007\/3-540-49116-3_30"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"T. Bultan. BDD vs. Constraint-Based Model Checking: An Experimental Evaluation for Asynchronous Concurrent Systems. Proc. of TACAS 2000, LNAI 1785, pp. 441\u2013455, 2000.","DOI":"10.1007\/3-540-46419-0_30"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"T. Bultan, R. Gerber, and W. Pugh. Symbolic Model Checking of Infinite-state Systems using Presburger Arithmetics. In Proc. of CAV 97, LNAI 1254, pp. 400\u2013411, 1997.","DOI":"10.1007\/3-540-63166-6_39"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"G. Ciardo. Petri nets with marking-dependent arc multiplicity: properties and analysis. In Proc. of ICATPN, LNAI 815, pp. 179\u2013198, 1994.","DOI":"10.1007\/3-540-58152-9_11"},{"issue":"5","key":"7_CR12","doi-asserted-by":"publisher","first-page":"726","DOI":"10.1145\/265943.265960","volume":"19","author":"E. Clarke","year":"1997","unstructured":"E. Clarke, O. Grumberg, S. Jha. Verifying Parameterized Networks. TOPLAS 19(5): 726\u2013750 (1997).","journal-title":"TOPLAS"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"P. Cousot and N. Halbwachs. Automatic Discovery of Linear Restraints among Variables of a Program. In Proc. of POPL 78, pp. 84\u201396, 1978.","DOI":"10.1145\/512760.512770"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"G. Delzanno. Automated Verification of Parameterized Cache Coherence Protocols. In Proc. CAV\u201900, LNAI 1855, pp. 53\u201368, 2000.","DOI":"10.1007\/10722167_8"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"G. Delzanno, J. Esparza, and A. Podelski. Constraint-based Analysis of Broadcast Protocols. In Proc. of CSL 99, LNAI 1683, pp. 50\u201366, 1999.","DOI":"10.1007\/3-540-48168-0_5"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"G. Delzanno and A. Podelski, Model Checking in CLP. In Proc. of TACAS 99, LNAI 1579, pp. 223\u2013239, 1999.","DOI":"10.1007\/3-540-49059-0_16"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"G. Delzanno, J.-F. Raskin, and L. Van Begin. Attacking Symbolic State Explosion. In Proc. CAV 2001, LNAI 2102, pages 298\u2013310, Springer, 2001.","DOI":"10.1007\/3-540-44585-4_28"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"G. Delzanno, J.-F. Raskin, and L. Van Begin. Towards the Automated Verification of Multithreaded Java Programs. To appear in TACAS 2002, April 2001.","DOI":"10.1007\/3-540-46002-0_13"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"E. A. Emerson and K. S. Namjoshi. Automatic Verification of Parameterized Synchronous Systems. In Proc. CAV 96, LNAI 1102, pp. 87\u201398, 1996.","DOI":"10.1007\/3-540-61474-5_60"},{"key":"7_CR20","doi-asserted-by":"crossref","unstructured":"E. A. Emerson and K. S. Namjoshi. On Model Checking for Non-deterministic Infinite-state Systems. In Proc. LICS 98, pp. 70\u201380, 1998.","DOI":"10.1109\/LICS.1998.705644"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"J. Esparza, A. Finkel, and R. Mayr. On the Verification of Broadcast Protocols. In Proc. LICS 99, pp. 352\u2013359, 1999.","DOI":"10.1109\/LICS.1999.782630"},{"issue":"1\u20132","key":"7_CR22","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","volume":"256","author":"A. Finkel","year":"2001","unstructured":"A. Finkel and Ph. Schnoebelen. Well-structured transition systems everywhere! Theoretical Computer Science, 256(1\u20132):63\u201392, 2001.","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"7_CR23","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"S. M. German","year":"1992","unstructured":"S. M. German, A. P. Sistla. Reasoning about Systems with Many Processes. JACM 39(3): 675\u2013735 (1992).","journal-title":"JACM"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"S. Graf and H. Sa\u00efdi. Construction of Abstract State Graphs with PVS. In Proc. of CAV 97, LNAI 1254, pp. 72\u201383, 1997.","DOI":"10.1007\/3-540-63166-6_10"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"N. Halbwachs. Delay analysis in synchronous programs. In Proc. CAV 93, LNAI 697, pp. 333\u2013346, 1993.","DOI":"10.1007\/3-540-56922-7_28"},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"N. Halbwachs and Y.-E. Proy and P. Raymond. Verification of Linear Hybrid Systems by Means of Convex Approximations. In Proc. SAS 94, LNAI 864, pp. 223\u2013237, 1994","DOI":"10.1007\/3-540-58485-4_43"},{"key":"7_CR27","unstructured":"J. Handy. The Cache Memory Book. Academic Press, 1993."},{"key":"7_CR28","doi-asserted-by":"crossref","unstructured":"T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. HYTECH: a Model Checker for Hybrid Systems. In Proc. CAV 97, LNAI 1254, pp. 460\u2013463, 1997.","DOI":"10.1007\/3-540-63166-6_48"},{"key":"7_CR29","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1016\/S0022-0000(69)80011-5","volume":"3","author":"R. M. Karp","year":"1969","unstructured":"R. M. Karp and R. E. Miller. Parallel Program Schemata. Journal of Computer and System Sciences, 3, pp. 147\u2013195, 1969.","journal-title":"Journal of Computer and System Sciences"},{"key":"7_CR30","doi-asserted-by":"crossref","unstructured":"R. P. Kurshan and K. McMillan. A Structural Induction Theorem for Processes. In Proc. 8th ACM Symp. on Principles of Distributed Computing, pp. 239\u2013247, 1989.","DOI":"10.1145\/72981.72998"},{"key":"7_CR31","doi-asserted-by":"crossref","unstructured":"D. Lesens and N. Halbwachs and P. Raymond. Automatic Verification of Parameterized Linear Networks of Processes. In Proc. of POPL 97, pp. 346\u2013357, 1997.","DOI":"10.1145\/263699.263747"},{"key":"7_CR32","doi-asserted-by":"crossref","unstructured":"D. Lesens and H. Saidi. Automatic Verification of Parameterized Networks of Processes by Abstraction. In Proc. INFINITY 97, 1997.","DOI":"10.1145\/263699.263747"},{"key":"7_CR33","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Verification of Infinite State Systems by Compositional Model Checking. In Proc. CHARME 99, LNAI 1703, pp. 219\u2013234, 1999.","DOI":"10.1007\/3-540-48153-2_17"},{"key":"7_CR34","unstructured":"A. Schrijver. Theory of Linear and Integer Programming. Wiley and Sons, 1998."},{"issue":"3\u20134","key":"7_CR35","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/BF01530796","volume":"8","author":"D. Srivistava","year":"1993","unstructured":"D. Srivistava. Subsumption and Indexing in Constraint Query Languages with Linear Arithmetic Constraints. Annals of Mathematics and Artificial Intelligence, 8(3\u20134): 315\u2013343, 1993.","journal-title":"Annals of Mathematics and Artificial Intelligence"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45988-X_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,17]],"date-time":"2025-01-17T01:17:21Z","timestamp":1737076641000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45988-X_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540433811","9783540459880"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/3-540-45988-x_7","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}