{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T08:11:39Z","timestamp":1760170299716},"reference-count":19,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2006,7,6]],"date-time":"2006-07-06T00:00:00Z","timestamp":1152144000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[2006,9]]},"DOI":"10.1007\/s10703-006-0011-4","type":"journal-article","created":{"date-parts":[[2006,7,6]],"date-time":"2006-07-06T04:43:46Z","timestamp":1152161026000},"page":"157-175","source":"Crossref","is-referenced-by-count":18,"title":["A work-efficient distributed algorithm for reachability analysis"],"prefix":"10.1007","volume":"29","author":[{"given":"Orna","family":"Grumberg","sequence":"first","affiliation":[]},{"given":"Tamir","family":"Heyman","sequence":"additional","affiliation":[]},{"given":"Assaf","family":"Schuster","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,7,6]]},"reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Amla N, Kurshan R, McMillan K, Medel RK (2003) Experimental analysis of different techniques for bounded model checking. In :Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'03), LNCS, Warsaw, Poland","DOI":"10.1007\/3-540-36577-X_4"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Beer I, Ben-David S, Eisner C, Landver A (1996) Rulebase: An industry-oriented formal verification tool. In: 33rd Design Automation Conf. pp 655\u2013660","DOI":"10.1109\/DAC.1996.545656"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Beer I, Ben-David S, Landver A (1998) On-the-Fly model checking of RCTL formulas. In: Proc. of the 10th Int. Conf. on Computer Aided Verification, pp 184\u2013194","DOI":"10.1007\/BFb0028744"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Biere A, Cimatti A, Clarke EM, Zhu Y (1999) Symbolic model checking without BDDs. In: Tools and Algorithms for the Construction and Analysis of Systems, 5th Int. Conference, TACAS'99, LNCS 1579","DOI":"10.21236\/ADA360973"},{"key":"11_CR5","unstructured":"Burch JR, Clarke EM, Long DE (1991) Symbolic model checking with partitioned transition relations. In Halaas A, Denyer PB (eds), Proc. of the 1991 Int. Conference on Very Large Scale Integration"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ (1992) Symbolic model checking: 1020 states and beyond. Inform Comput 98(2):142\u2013171","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Cabodi G (2001) Meta-BDDs: A decomposed representation for layered symbolic manipulation of boolean functions. In: Proc. of the 13th Int. Conf. on Computer Aided Verification, LNCS","DOI":"10.1007\/3-540-44585-4_11"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Cabodi G, Camurati P, Quer S (1996) Improved reachability analysis of large FSM. In: Proc. of the IEEE Int. Conf. on Computer Aided Design, IEEE Computer Society Press, pp 354\u2013360","DOI":"10.1109\/ICCAD.1996.569819"},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"Cabodi G, Camurati P, Quer S (1999) Improving the efficient of BDD-based operators by means of partitioning. IEEE Trans Comput-Aid Design","DOI":"10.1109\/43.759068"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"Cimatti A, Clarke EM, Giunchiglia F, Roveri M (1999) NUSMV: A new symbolic model verifier. In: Halbwachs N, Peled D (eds) Proc. of the 7th Int. Conf. on Computer-Aided Verification (CAV'99), LNCS 1633, Trento, Italy, pp 495\u2013499","DOI":"10.1007\/3-540-48683-6_44"},{"key":"11_CR11","unstructured":"Geist D, Beer I (1994) Efficient model checking by automated ordering of transition relation partitions. In: Proc. of the Sixth Int. Conf. on Computer Aided Verification, LNCS 818, pp 299\u2013310"},{"key":"11_CR12","unstructured":"Grumberg O, Heyman A, Heyman T, Schuster A (2003) Division system: A general platform for distributed symbolic model checking research. http:\/\/www.cs.technion.ac.il\/Labs\/dsl\/projects\/division web\/division.htm"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"Heyman T, Geist D, Grumberg O, Schuster A (2002) Achieving scalability in parallel reachability analysis of very large circuits. Formal Methods System Design 21(2):317\u2013338","DOI":"10.1023\/A:1020373206491"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"McMillan KL (1993) Symbolic model checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Milvang-Jensen K, Hu AJ (1998) BDDNOW: A parallel BDD package. In: Second Int. Conference on Formal methods in Computer-Aided Design (FMCAD'98), LNCS, Palo Alto, California, USA","DOI":"10.1007\/3-540-49519-3_32"},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"Narayan A, Isles A, Jain J, Brayton R, Sangiovanni-Vincentelli AL (1997) Reachability analysis using partitioned-ROBDDs. In: Proc. of the IEEE Int. Conf. on Computer Aided Design, IEEE Computer Society Press, pp 388\u2013393","DOI":"10.1109\/ICCAD.1997.643565"},{"key":"11_CR17","doi-asserted-by":"crossref","unstructured":"Narayan A, Jain J, Fujita M, Sangiovanni-Vincentelli AL (1996) Partitioned-ROBDDs. In: Proc. of the IEEE Int. Conf. on Computer Aided Design, IEEE Computer Society Press, pp 547\u2013554","DOI":"10.1109\/ICCAD.1996.569909"},{"key":"11_CR18","unstructured":"Stern U, David L Dill (1997) Parallelizing the murphy verifier. In: Proc. of the 9th Int. Conf. on Computer Aided Verification, LNCS 1254, pp 256\u2013267"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Stornetta T, Brewer F (1996) Implementation of an efficient parallel BDD package. In: 33rd Design Automation Conf. IEEE Computer Society Press","DOI":"10.1145\/240518.240639"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-006-0011-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-006-0011-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-006-0011-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T22:01:02Z","timestamp":1559253662000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-006-0011-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,7,6]]},"references-count":19,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2006,9]]}},"alternative-id":["11"],"URL":"https:\/\/doi.org\/10.1007\/s10703-006-0011-4","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2006,7,6]]}}}