{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,17]],"date-time":"2025-09-17T16:55:04Z","timestamp":1758128104710,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":37,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642195822"},{"type":"electronic","value":"9783642195839"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-19583-9_9","type":"book-chapter","created":{"date-parts":[[2011,3,9]],"date-time":"2011-03-09T04:16:56Z","timestamp":1299644216000},"page":"46-59","source":"Crossref","is-referenced-by-count":4,"title":["Parallelizing a Symbolic Compositional Model-Checking Algorithm"],"prefix":"10.1007","author":[{"given":"Ariel","family":"Cohen","sequence":"first","affiliation":[]},{"given":"Kedar S.","family":"Namjoshi","sequence":"additional","affiliation":[]},{"given":"Yaniv","family":"Sa\u2019ar","sequence":"additional","affiliation":[]},{"given":"Lenore D.","family":"Zuck","sequence":"additional","affiliation":[]},{"given":"Katya I.","family":"Kisyova","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/3-540-44585-4_19","volume-title":"Computer Aided Verification","author":"T. Arons","year":"2001","unstructured":"Arons, T., Pnueli, A., Ruah, S., Xu, J., Zuck, L.D.: Parameterized verification with automatically computed inductive assertions. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 221\u2013234. Springer, Heidelberg (2001)"},{"key":"9_CR2","unstructured":"Burch, J.R., Clarke, E.M., Long, D.E.: Symbolic model checking with partitioned transistion relations. In: VLSI (1991)"},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Cabodi, G., Camurati, P., Lioy, A., Poncino, M., Quer, S.: A parallel approach to symbolic traversal based on set partitioning. In: CHARME, pp. 167\u2013184 (1997)","DOI":"10.1007\/978-0-387-35190-2_11"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Cabodi, G., Camurati, P., Quer, S.: Improved reachability analysis of large finite state machines. In: ICCAD, pp. 354\u2013360 (1996)","DOI":"10.1109\/ICCAD.1996.569819"},{"issue":"12","key":"9_CR5","doi-asserted-by":"publisher","first-page":"1465","DOI":"10.1109\/43.552080","volume":"15","author":"H. Cho","year":"1996","unstructured":"Cho, H., Hachtel, G.D., Macii, E., Plessier, B., Somenzi, F.: Algorithms for approximate fsm traversal based on state space decomposition. IEEE Trans. on CAD of Integrated Circuits and Systems\u00a015(12), 1465\u20131478 (1996)","journal-title":"IEEE Trans. on CAD of Integrated Circuits and Systems"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-540-73368-3_9","volume-title":"Computer Aided Verification","author":"A. Cohen","year":"2007","unstructured":"Cohen, A., Namjoshi, K.S.: Local proofs for global safety properties. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 55\u201367. Springer, Heidelberg (2007)"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-540-70545-1_15","volume-title":"Computer Aided Verification","author":"A. Cohen","year":"2008","unstructured":"Cohen, A., Namjoshi, K.S.: Local proofs for linear-time properties of concurrent programs. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 149\u2013161. Springer, Heidelberg (2008)"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1007\/978-3-642-14295-6_46","volume-title":"Computer Aided Verification","author":"A. Cohen","year":"2010","unstructured":"Cohen, A., Namjoshi, K.S., Sa\u2019ar, Y.: A dash of fairness for compositional reasoning. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 543\u2013557. Springer, Heidelberg (2010)"},{"key":"9_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1007\/978-3-642-14295-6_47","volume-title":"Computer Aided Verification","author":"A. Cohen","year":"2010","unstructured":"Cohen, A., Namjoshi, K.S., Sa\u2019ar, Y.: Split: A compositional LTL verifier. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 558\u2013561. Springer, Heidelberg (2010)"},{"key":"9_CR10","unstructured":"Cohen, A., Namjoshi, K.S., Sa\u2019ar, Y., Zuck, L.D., Kisyova, K.I.: Model checking in bits and pieces. In: EC2 Workshop, CAV (2010), http:\/\/split.ysaar.net\/data\/EC2.pdf"},{"key":"9_CR11","unstructured":"Cousot, P.: Asynchronous iterative methods for solving a fixed point system of monotone equations in a complete lattice. Res. rep. R.R. 88, Laboratoire IMAG, Universit\u00e9 scientifique et m\u00e9dicale de Grenoble, Grenoble, France (September 1977)"},{"key":"9_CR12","first-page":"1","volume-title":"ACM Symposium on Artificial Intelligence & Programming Languages","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Automatic synthesis of optimal invariant assertions: mathematical foundations. In: ACM Symposium on Artificial Intelligence & Programming Languages, vol.\u00a012(8), pp. 1\u201312. ACM SIGPLAN Not, Rochester, NY (August 1977)"},{"key":"9_CR13","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-3228-5","volume-title":"Predicate Calculus and Program Semantics","author":"E.W. Dijkstra","year":"1990","unstructured":"Dijkstra, E.W., Scholten, C.S.: Predicate Calculus and Program Semantics. Springer, Heidelberg (1990)"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/978-3-540-73368-3_31","volume-title":"Computer Aided Verification","author":"J. Ezekiel","year":"2007","unstructured":"Ezekiel, J., L\u00fcttgen, G., Ciardo, G.: Parallelising symbolic state-space generators. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 268\u2013280. Springer, Heidelberg (2007)"},{"key":"9_CR15","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":"9_CR16","unstructured":"German, S., Janssen, G.: A tutorial example of a cache memory protocol and RTL implementation. Technical Report RC23958 (W0605-092), IBM, 5 (2006)"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Govindaraju, S.G., Dill, D.L., Hu, A.J., Horowitz, M.: Approximate reachability with bdds using overlapping projections. In: DAC, pp. 451\u2013456 (1998)","DOI":"10.1145\/277044.277169"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1007\/11560548_12","volume-title":"Correct Hardware Design and Verification Methods","author":"O. Grumberg","year":"2005","unstructured":"Grumberg, O., Heyman, T., Ifergan, N., Schuster, A.: Achieving speedups in distributed symbolic reachability analysis through asynchronous computation. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol.\u00a03725, pp. 129\u2013145. Springer, Heidelberg (2005)"},{"issue":"2","key":"9_CR19","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/s10703-006-0011-4","volume":"29","author":"O. Grumberg","year":"2006","unstructured":"Grumberg, O., Heyman, T., Schuster, A.: A work-efficient distributed algorithm for reachability analysis. Formal Methods in System Design\u00a029(2), 157\u2013175 (2006)","journal-title":"Formal Methods in System Design"},{"issue":"10","key":"9_CR20","doi-asserted-by":"publisher","first-page":"659","DOI":"10.1109\/TSE.2007.70724","volume":"33","author":"G.J. Holzmann","year":"2007","unstructured":"Holzmann, G.J., Bosnacki, D.: The design of a multicore extension of the SPIN model checker. IEEE Trans. Software Eng.\u00a033(10), 659\u2013674 (2007)","journal-title":"IEEE Trans. Software Eng."},{"key":"9_CR21","first-page":"1","volume-title":"IPDPS","author":"G.J. Holzmann","year":"2007","unstructured":"Holzmann, G.J., Bosnacki, D.: Multi-core model checking with SPIN. In: IPDPS, pp. 1\u20138. IEEE, Los Alamitos (2007)"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/3-540-56922-7_2","volume-title":"Computer Aided Verification","author":"A.J. Hu","year":"1993","unstructured":"Hu, A.J., Dill, D.L.: Efficient verification with bdds using implicitly conjoined invariants. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 3\u201314. Springer, Heidelberg (1993)"},{"issue":"5","key":"9_CR23","doi-asserted-by":"publisher","first-page":"780","DOI":"10.1109\/TCAD.2006.870410","volume":"25","author":"S.K. Iyer","year":"2006","unstructured":"Iyer, S.K., Sahoo, D., Emerson, E.A., Jain, J.: On partitioning and symbolic model checking. IEEE Trans. on CAD of Integrated Circuits and Systems\u00a025(5), 780\u2013788 (2006)","journal-title":"IEEE Trans. on CAD of Integrated Circuits and Systems"},{"key":"9_CR24","doi-asserted-by":"crossref","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Software Eng.\u00a03(2) (1977)","DOI":"10.1109\/TSE.1977.229904"},{"key":"9_CR25","unstructured":"L\u00fcttgen, G.: Parallelising Symbolic State-Space Generators: Frustration & Hope. Seminar on Distributed Verification and Grid Computing. Schloss Dagstuhl, Germany (August 2008), http:\/\/www-users.cs.york.ac.uk\/~luettgen\/presentations"},{"key":"9_CR26","unstructured":"Moon, I.-H., Kukula, J.H., Shiple, T.R., Somenzi, F.: Least fixpoint approximations for reachability analysis. In: ICCAD, pp. 41\u201344 (1999)"},{"key":"9_CR27","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":"9_CR28","doi-asserted-by":"crossref","unstructured":"Narayan, A., Isles, A.J., Jain, J., Brayton, R.K., Sangiovanni-Vincentelli, A.L.: Reachability analysis using partitioned-robdds. In: ICCAD, pp. 388\u2013393 (1997)","DOI":"10.1109\/ICCAD.1997.643565"},{"issue":"5","key":"9_CR29","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1145\/360051.360224","volume":"19","author":"S.S. Owicki","year":"1976","unstructured":"Owicki, S.S., Gries, D.: Verifying properties of parallel programs: An axiomatic approach. ACM Commun.\u00a019(5), 279\u2013285 (1976)","journal-title":"ACM Commun."},{"issue":"3","key":"9_CR30","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1016\/0020-0190(81)90106-X","volume":"12","author":"G.L. Peterson","year":"1981","unstructured":"Peterson, G.L.: Myths about the mutual exclusion problem. Inf. Process. Lett.\u00a012(3), 115\u2013116 (1981)","journal-title":"Inf. Process. Lett."},{"key":"9_CR31","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.: Automatic deductive verification with invisible invariants. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 82\u201397. Springer, Heidelberg (2001)"},{"key":"9_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-14295-6_18","volume-title":"Computer Aided Verification","author":"A. Pnueli","year":"2010","unstructured":"Pnueli, A., Sa\u2019ar, Y., Zuck, L.D.: jtlv: A framework for developing verification algorithms. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 171\u2013174. Springer, Heidelberg (2010), http:\/\/jtlv.sourceforge.net\/"},{"key":"9_CR33","doi-asserted-by":"crossref","unstructured":"Ravi, K., Somenzi, F.: High-density reachability analysis. In: ICCAD, pp. 154\u2013158 (1995)","DOI":"10.1109\/ICCAD.1995.480006"},{"key":"9_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/11562948_5","volume-title":"Automated Technology for Verification and Analysis","author":"D. Sahoo","year":"2005","unstructured":"Sahoo, D., Jain, J., Iyer, S.K., Dill, D.L.: A new reachability algorithm for symmetric multi-processor architecture. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol.\u00a03707, pp. 26\u201338. Springer, Heidelberg (2005)"},{"key":"9_CR35","first-page":"467","volume-title":"DAC","author":"D. Sahoo","year":"2005","unstructured":"Sahoo, D., Jain, J., Iyer, S.K., Dill, D.L., Emerson, E.A.: Multi-threaded reachability. In: DAC, pp. 467\u2013470. ACM, New York (2005)"},{"issue":"2","key":"9_CR36","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1023\/A:1008771324652","volume":"18","author":"U. Stern","year":"2001","unstructured":"Stern, U., Dill, D.L.: Parallelizing the Mur\u03d5 verifier. Formal Methods in System Design\u00a018(2), 117\u2013129 (2001)","journal-title":"Formal Methods in System Design"},{"key":"9_CR37","first-page":"621","volume-title":"Proc. 1988 International Conference on Supercomputing Systems","author":"B.K. Szymanski","year":"1988","unstructured":"Szymanski, B.K.: A simple solution to Lamport\u2019s concurrent programming problem with linear wait. In: Proc. 1988 International Conference on Supercomputing Systems, pp. 621\u2013626. St. Malo, France (1988)"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software: Verification and Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-19583-9_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,3]],"date-time":"2025-03-03T22:06:41Z","timestamp":1741039601000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-19583-9_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642195822","9783642195839"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-19583-9_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}