{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,11]],"date-time":"2026-11-11T20:34:34Z","timestamp":1794429274817,"version":"4.9.1"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642331244","type":"print"},{"value":"9783642331251","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33125-1_12","type":"book-chapter","created":{"date-parts":[[2012,8,29]],"date-time":"2012-08-29T02:47:24Z","timestamp":1346208444000},"page":"146-163","source":"Crossref","is-referenced-by-count":16,"title":["Invariant Generation for Parametrized Systems Using Self-reflection"],"prefix":"10.1007","author":[{"given":"Alejandro","family":"Sanchez","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sriram","family":"Sankaranarayanan","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"C\u00e9sar","family":"S\u00e1nchez","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bor-Yuh Evan","family":"Chang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/3-540-48683-6_14","volume-title":"Computer Aided Verification","author":"P.A. Abdulla","year":"1999","unstructured":"Abdulla, P.A., Bouajjani, A., Jonsson, B., Nilsson, M.: Handling Global Conditions in Parameterized System Verification. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 134\u2013145. Springer, Heidelberg (1999)"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1007\/978-3-540-73368-3_17","volume-title":"Computer Aided Verification","author":"P.A. Abdulla","year":"2007","unstructured":"Abdulla, P.A., Delzanno, G., Rezine, A.: Parameterized Verification of Infinite-State Processes with Global Conditions. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 145\u2013157. Springer, Heidelberg (2007)"},{"issue":"6","key":"12_CR3","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"22","author":"K.R. Apt","year":"1986","unstructured":"Apt, K.R., Kozen, D.C.: Limits for automatic verification of finite-state concurrent systems. Info. Proc. Letters\u00a022(6), 307\u2013309 (1986)","journal-title":"Info. Proc. Letters"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/978-3-540-70545-1_37","volume-title":"Computer Aided Verification","author":"J. Berdine","year":"2008","unstructured":"Berdine, J., Lev-Ami, T., Manevich, R., Ramalingam, G., Sagiv, M.: Thread Quantification for Concurrent Shape Analysis. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 399\u2013413. Springer, Heidelberg (2008)"},{"key":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-36377-7_5","volume-title":"The Essence of Computation","author":"B. Blanchet","year":"2002","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software. In: Mogensen, T.\u00c6., Schmidt, D.A., Hal Sudborough, I. (eds.) The Essence of Computation. LNCS, vol.\u00a02566, pp. 85\u2013108. Springer, Heidelberg (2002)"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/3-540-46002-0_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Bozzano","year":"2002","unstructured":"Bozzano, M., Delzanno, G.: Beyond Parameterized Verification. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 221\u2013235. Springer, Heidelberg (2002)"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Browne, M.C.: Reasoning about networks with many identical finite-state processes. In: PODC 1986, pp. 240\u2013248. ACM (1986)","DOI":"10.1145\/10590.10611"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/3-540-60218-6_30","volume-title":"CONCUR \u201995 Concurrency Theory","author":"E.M. Clarke","year":"1995","unstructured":"Clarke, E.M., Grumberg, O., Jha, S.: Veryfying Parameterized Networks using Abstraction and Regular Languages. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol.\u00a0962, pp. 395\u2013407. Springer, Heidelberg (1995)"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-78800-3_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Clarke","year":"2008","unstructured":"Clarke, E., Talupur, M., Veith, H.: Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 33\u201347. Springer, Heidelberg (2008)"},{"issue":"2","key":"12_CR10","doi-asserted-by":"publisher","first-page":"104","DOI":"10.4028\/www.scientific.net\/MSF.610-613.104","volume":"34","author":"A. Cohen","year":"2009","unstructured":"Cohen, A., Namjoshi, K.S.: Local proofs for global safety properties. FMSD\u00a034(2), 104\u2013125 (2009)","journal-title":"FMSD"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-540-45069-6_39","volume-title":"Computer Aided Verification","author":"M.A. Col\u00f3n","year":"2003","unstructured":"Col\u00f3n, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear Invariant Generation Using Non-linear Constraint Solving. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 420\u2013432. Springer, Heidelberg (2003)"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Correll, N., Martinoli, A.: Collective inspection of regular structures using a swarm of miniature robots. In: ISER. Springer Tracts in Advanced Robotics, vol.\u00a021, pp. 375\u2013386. Springer (2004)","DOI":"10.1007\/11552246_36"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract Interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL 1977, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"12_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/3-540-55844-6_142","volume-title":"Programming Language Implementation and Logic Programming","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Comparing the Galois Connection and Widening\/Narrowing Approaches to Abstract Interpretation (Invited Paper). In: Bruynooghe, M., Wirsing, M. (eds.) PLILP 1992. LNCS, vol.\u00a0631, pp. 269\u2013295. Springer, Heidelberg (1992)"},{"key":"12_CR15","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/10721959_19","volume-title":"Automated Deduction - CADE-17","author":"E. Allen Emerson","year":"2000","unstructured":"Allen Emerson, E., Kahlon, V.: Reducing Model Checking of the Many to the Few. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol.\u00a01831, pp. 236\u2013254. Springer, Heidelberg (2000)"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/3-540-61474-5_60","volume-title":"Computer Aided Verification","author":"E.A. Emerson","year":"1996","unstructured":"Emerson, E.A., Namjoshi, K.S.: Automatic Verification of Parameterized Synchronous Systems. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 87\u201398. Springer, Heidelberg (1996)"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Farzan, A., Kincaid, Z.: Verification of parameterized concurrent programs by modular reasoning about data and control. In: POPL 2012, pp. 297\u2013308. ACM (2012)","DOI":"10.1145\/2103621.2103693"},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-44829-2_14","volume-title":"Model Checking Software","author":"C. Flanagan","year":"2003","unstructured":"Flanagan, C., Qadeer, S.: Thread-Modular Model Checking. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 213\u2013224. Springer, Heidelberg (2003)"},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-540-71316-6_17","volume-title":"Programming Languages and Systems","author":"S. Gaubert","year":"2007","unstructured":"Gaubert, S., Goubault, \u00c9., Taly, A., Zennou, S.: Static Analysis by Policy Iteration on Relational Domains. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 237\u2013252. Springer, Heidelberg (2007)"},{"key":"12_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/978-3-540-71316-6_21","volume-title":"Programming Languages and Systems","author":"T. Gawlitza","year":"2007","unstructured":"Gawlitza, T., Seidl, H.: Precise Fixpoint Computation Through Strategy Iteration. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 300\u2013315. Springer, Heidelberg (2007)"},{"issue":"3","key":"12_CR21","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"S.M. German","year":"1992","unstructured":"German, S.M., Sistla, A.P.: Reasoning about systems with many processes. J. of the ACM\u00a039(3), 675\u2013735 (1992)","journal-title":"J. of the ACM"},{"key":"12_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-540-45069-6_27","volume-title":"Computer Aided Verification","author":"T.A. Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Qadeer, S.: Thread-Modular Abstraction Refinement. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 262\u2013274. Springer, Heidelberg (2003)"},{"key":"12_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/978-3-642-02658-4_52","volume-title":"Computer Aided Verification","author":"B. Jeannet","year":"2009","unstructured":"Jeannet, B., Min\u00e9, A.: Apron: A Library of Numerical Abstract Domains for Static Analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 661\u2013667. Springer, Heidelberg (2009)"},{"key":"12_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-642-00768-2_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"V. Kahlon","year":"2009","unstructured":"Kahlon, V., Sankaranarayanan, S., Gupta, A.: Semantic Reduction of Thread Interleavings in Concurrent Programs. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 124\u2013138. Springer, Heidelberg (2009)"},{"key":"12_CR25","doi-asserted-by":"crossref","unstructured":"Lesens, D., Halbwachs, N., Raymond, P.: Automatic verification of parameterized linear networks of processes. In: POPL 1997, pp. 346\u2013357. ACM (1997)","DOI":"10.1145\/263699.263747"},{"key":"12_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-540-74061-2_14","volume-title":"Static Analysis","author":"A. Malkis","year":"2007","unstructured":"Malkis, A., Podelski, A., Rybalchenko, A.: Precise Thread-Modular Verification. In: Riis Nielson, H., Fil\u00e9, G. (eds.) SAS 2007. LNCS, vol.\u00a04634, pp. 218\u2013232. Springer, Heidelberg (2007)"},{"key":"12_CR27","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer (1995)","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"12_CR28","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-642-23702-7_20","volume-title":"Static Analysis","author":"K.L. McMillan","year":"2011","unstructured":"McMillan, K.L., Zuck, L.D.: Invisible Invariants and Abstract Interpretation. In: Yahav, E. (ed.) SAS 2011. LNCS (LNAI), vol.\u00a06887, pp. 249\u2013262. Springer, Heidelberg (2011)"},{"key":"12_CR29","unstructured":"Mellor-Crummey, J.M., Scott, M.L.: Barriers for the sequent symmetry, \n                    \n                      ftp:\/\/ftp.cs.rochester.edu\/pub\/packages\/scalable_synch\/locks_and_barriers\/Symmetry.tar.Z"},{"key":"12_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-3-642-19718-5_21","volume-title":"Programming Languages and Systems","author":"A. Min\u00e9","year":"2011","unstructured":"Min\u00e9, A.: Static Analysis of Run-Time Errors in Embedded Critical Parallel C Programs. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol.\u00a06602, pp. 398\u2013418. Springer, Heidelberg (2011)"},{"key":"12_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-540-69738-1_22","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"K.S. Namjoshi","year":"2007","unstructured":"Namjoshi, K.S.: Symmetry and Completeness in the Analysis of Parameterized Systems. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 299\u2013313. Springer, Heidelberg (2007)"},{"key":"12_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-45319-9_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Pnueli","year":"2001","unstructured":"Pnueli, A., Ruah, S., Zuck, L.D.: Automatic Deductive Verification with Invisible Invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 82\u201397. Springer, Heidelberg (2001)"},{"issue":"1","key":"12_CR33","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/271510.271517","volume":"20","author":"M. Sagiv","year":"1998","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Solving shape-analysis problems in languages with destructive updating. ACM Trans. Program. Lang. Syst.\u00a020(1), 1\u201350 (1998)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"12_CR34","doi-asserted-by":"crossref","unstructured":"Sanchez, A., Sankaranarayanan, S., S\u00e1nchez, C., Chang, B.Y.E.: Invariant generation for parametrized systems using self-reflection (extended version). Tech. Rep. CU-CS-1094-12, University of Colorado Boulder (2012)","DOI":"10.1007\/978-3-642-33125-1_12"},{"key":"12_CR35","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/j.cl.2004.02.006","volume":"30","author":"L.D. Zuck","year":"2004","unstructured":"Zuck, L.D., Pnueli, A.: Model checking and abstraction to the aid of parameterized systems (a survey). Computer Languages, Systems & Structures\u00a030, 139\u2013169 (2004)","journal-title":"Computer Languages, Systems & Structures"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33125-1_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T07:56:09Z","timestamp":1620114969000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33125-1_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642331244","9783642331251"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33125-1_12","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-642-33125-1","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}