{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:27:53Z","timestamp":1761611273760},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540203636"},{"type":"electronic","value":"9783540397243"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-39724-3_30","type":"book-chapter","created":{"date-parts":[[2011,1,7]],"date-time":"2011-01-07T21:15:55Z","timestamp":1294434955000},"page":"334-347","source":"Crossref","is-referenced-by-count":8,"title":["Efficient Distributed SAT and SAT-Based Distributed Bounded Model Checking"],"prefix":"10.1007","author":[{"given":"Malay K","family":"Ganai","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zijiang","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pranav","family":"Ashar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"30_CR1","unstructured":"Silburt, A., Evans, A., Vrckovik, G., Diufrensne, M., Brown, T.: Functional Verification of ASICs in Silicon Intensive Systems. Presented at DesignCon 1998 On-Chip System Design Conference (1998)"},{"key":"30_CR2","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"30_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking: An Approach to the State Explosion Problem","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, Dordrecht (1993)"},{"issue":"8","key":"30_CR4","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers\u00a0C-35(8), 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers"},{"key":"30_CR5","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: Proceedings of the Design Automation Conference, pp. 317\u2013320 (1999)","DOI":"10.21236\/ADA360973"},{"key":"30_CR6","doi-asserted-by":"crossref","unstructured":"Bjesse, P., Claessen, K.: SAT-based verification without state space traversal. In: Proceedings of Conference on Formal Methods in Computer-Aided Design (2000)","DOI":"10.1007\/3-540-40922-X_23"},{"key":"30_CR7","doi-asserted-by":"crossref","unstructured":"Ganai, M., Aziz, A.: Improved SAT-based Bounded Reachability Analysis. In: Proceedings of VLSI Design Conference (2002)","DOI":"10.1109\/ASPDAC.2002.995020"},{"key":"30_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1007\/3-540-46419-0_28","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P.A. Abdulla","year":"2000","unstructured":"Abdulla, P.A., Bjesse, P., Een, N.: Symbolic Reachability Analysis based on {SAT}- Solvers. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol.\u00a01785, p. 411. Springer, Heidelberg (2000)"},{"key":"30_CR9","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J.P. Marques-Silva","year":"1999","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP: A Search Algorithm for Propositional Satisfiability. IEEE Transactions on Computers\u00a048, 506\u2013521 (1999)","journal-title":"IEEE Transactions on Computers"},{"key":"30_CR10","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1007\/3-540-63104-6_28","volume-title":"Automated Deduction - CADE-14","author":"H. Zhang","year":"1997","unstructured":"Zhang, H.: SATO: An efficient propositional prover. In: McCune, W. (ed.) CADE 1997. LNCS (LNAI), vol.\u00a01249, pp. 272\u2013275. Springer, Heidelberg (1997)"},{"key":"30_CR11","doi-asserted-by":"crossref","unstructured":"Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proceedings of Design Automation Conference (2001)","DOI":"10.1145\/378239.379017"},{"key":"30_CR12","doi-asserted-by":"crossref","unstructured":"Ganai, M., Zhang, L., Ashar, P., Gupta, A.: Combining Strengths of Circuit-based and CNF-based Algorithms for a High Performance SAT Solver. In: Proceedings of the Design Automation Conference (2002)","DOI":"10.1145\/513918.514105"},{"key":"30_CR13","doi-asserted-by":"crossref","unstructured":"Kuehlmann, A., Ganai, M., Paruthi, V.: Circuit-based Boolean Reasoning. In: Proceedings of Design Automation Conference (2001)","DOI":"10.1145\/378239.378470"},{"key":"30_CR14","doi-asserted-by":"crossref","unstructured":"Wah, B.W., Li, G.-J., Yu, C.F.: Multiprocessing of Combinational Search Problems. IEEE computer, 93\u2013108 (1985)","DOI":"10.1109\/MC.1985.1662926"},{"key":"30_CR15","doi-asserted-by":"crossref","unstructured":"Zhang, H., Bonacina, M.P., Hsiang, J.: PSATO: a Distributed Propositional Prover and its Application to Quasigroup Problems. Journal of Symbolic Computation (1996)","DOI":"10.1006\/jsco.1996.0030"},{"key":"30_CR16","doi-asserted-by":"crossref","unstructured":"Zhao, Y.: Accelerating Boolean Satisfiability through Application Specific Processing, Ph.D. Thesis. Princeton (2001)","DOI":"10.1145\/500001.500059"},{"key":"30_CR17","volume-title":"Parallel Algorithms for Machine Intelligence and Vision","author":"C. Powley","year":"1990","unstructured":"Powley, C., Fergusion, C., Korf, R.: Parallel Heuristic Search: Two Approaches. In: Kumar, V., Gopalakrishnan, P.S., Kanal, L.N. (eds.) Parallel Algorithms for Machine Intelligence and Vision, Springer, New York (1990)"},{"key":"30_CR18","doi-asserted-by":"crossref","unstructured":"Jurkowiak, B., Li, C.M., Utard, G.: Parallelizing Satz Using Dynamic Workload Balancing. Presented at Workshop on Theory and Applications of Satisfiability Testing (2001)","DOI":"10.1016\/S1571-0653(04)00321-X"},{"key":"30_CR19","unstructured":"Boehm, M., Speckenmeyer, E.: A Fast Parallel SAT-solver \u2013 Efficient Workload Balancing. Presented at Third International Symposium on Artificial Intelligence and Mathematics, Fort Lauderdale, Florida (1994)"},{"key":"30_CR20","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"U. Stern","year":"1997","unstructured":"Stern, U., Dill, D.L.: Parallelizing the Murphi Verifier. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, Springer, Heidelberg (1997)"},{"key":"30_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_6","volume-title":"Computer Aided Verification","author":"T. Heyman","year":"2000","unstructured":"Heyman, T., Geist, D., Grumberg, O., Schuster, A.: Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, Springer, Heidelberg (2000)"},{"key":"30_CR22","doi-asserted-by":"crossref","unstructured":"Narayan, A., Isles, A., Jain, J., Brayton, R., Sangiovanni-Vincentelli, A.L.: Reachability Analysis using Partitioned-ROBDDs. Presented at International Conference on Computer-Aided Design (1997)","DOI":"10.1109\/ICCAD.1997.643565"},{"key":"30_CR23","unstructured":"Yadgar, A.: Parallel SAT Solving for Model Checking (2002), http:\/\/www.cs.technion.ac.il\/~adgar\/Research\/research.pdf"},{"key":"30_CR24","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Longeman, G., Loveland, D.: A Machine Program for Theorem Proving. Communications of the ACM\u00a05, 394\u2013397 (1962)","journal-title":"Communications of the ACM"},{"key":"30_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic Model Checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, p. 193. Springer, Heidelberg (1999)"},{"key":"30_CR26","doi-asserted-by":"crossref","unstructured":"Sheeran, M., Singh, S., Stalmarck, G.: Checking Safety Properties using Induction and a SAT Solver. In: Proceedings of Conference on Formal Methods in Computer-Aided Design (2000)","DOI":"10.1007\/3-540-40922-X_8"},{"issue":"1","key":"30_CR27","first-page":"60","volume":"44","author":"A. Hasegawa","year":"2003","unstructured":"Hasegawa, A., Matsuoka, H., Nakanishi, K.: Clustering Software for Linux-Based HPC. NEC Research & Development\u00a044(1), 60\u201363 (2003)","journal-title":"NEC Research & Development"}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-39724-3_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T14:03:42Z","timestamp":1559916222000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39724-3_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540203636","9783540397243"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39724-3_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}