{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,14]],"date-time":"2023-09-14T17:28:40Z","timestamp":1694712520334},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"4-5","license":[{"start":{"date-parts":[[2006,4,5]],"date-time":"2006-04-05T00:00:00Z","timestamp":1144195200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2006,8]]},"DOI":"10.1007\/s10009-005-0203-z","type":"journal-article","created":{"date-parts":[[2006,9,20]],"date-time":"2006-09-20T09:04:54Z","timestamp":1158743094000},"page":"387-396","source":"Crossref","is-referenced-by-count":5,"title":["Efficient distributed SAT and SAT-based distributed Bounded Model Checking"],"prefix":"10.1007","volume":"8","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","published-online":{"date-parts":[[2006,4,5]]},"reference":[{"key":"203_CR1","unstructured":"Silburt, A., Evans, A., Vrckovik, G., Diufrensne, M., Brown, T.: Functional verification of ASICs in silicon intensive systems. Presented at DesignCon98 On-Chip System Design Conference (1998)"},{"key":"203_CR2","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)"},{"key":"203_CR3","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, Drodrecht (1993)","DOI":"10.1007\/978-1-4615-3190-6_3"},{"issue":"8","key":"203_CR4","doi-asserted-by":"crossref","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 Trans. Comput. C-35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"key":"203_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":"203_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":"203_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":"203_CR8","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Bjesse, P., Een, N.: Symbolic reachability analysis based on SAT-solvers. In: Proceedings of Workshop on Tools and Algorithms for the Analysis and Construction of Systems (TACAS) (2000)","DOI":"10.1007\/3-540-46419-0_28"},{"key":"203_CR9","doi-asserted-by":"crossref","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 Trans. Comput. 48, 506\u2013521 (1999)","journal-title":"IEEE Trans. Comput."},{"key":"203_CR10","doi-asserted-by":"crossref","unstructured":"Zhang, H.: SATO: An efficient propositional prover. In: Proceedings of International Conference on Automated Deduction, LNAI, vol. 1249, pp. 272\u2013275 (1997)","DOI":"10.1007\/3-540-63104-6_28"},{"key":"203_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":"203_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":"203_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":"203_CR14","doi-asserted-by":"crossref","unstructured":"Wah, B.W., Li, G.-J., Yu, C.F.: Multiprocessing of combinational search problems. IEEE Comput. 93\u2013108 (1985)","DOI":"10.1109\/MC.1985.1662926"},{"key":"203_CR15","doi-asserted-by":"crossref","unstructured":"Zhang, H., Bonacina, M.P., Hsiang, J.: PSATO: A distributed propositional prover and its application to quasigroup problems. J. Symbol. Comput. (1996)","DOI":"10.1006\/jsco.1996.0030"},{"key":"203_CR16","doi-asserted-by":"crossref","unstructured":"Zhao, Y.: Accelerating Boolean satisfiability through application specific processing. Ph.D. thesis, Princeton (2001)","DOI":"10.1145\/500058.500059"},{"key":"203_CR17","doi-asserted-by":"crossref","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-Verlag, New York (1990)","DOI":"10.1007\/978-1-4612-3390-9_2"},{"key":"203_CR18","doi-asserted-by":"crossref","unstructured":"Jurkowiak, B., Li, C.M., Utard, G.: Parallelizing Satz using dynamic workload balancing. In: Presented at Workshop on Theory and Applications of Satisfiability Testing (2001)","DOI":"10.1016\/S1571-0653(04)00321-X"},{"key":"203_CR19","unstructured":"Boehm, M., Speckenmeyer, E.: A fast parallel SAT-solver\u2014Efficient workload balancing. In: Presented at Third International Symposium on Artificial Intelligence and Mathematics. Fort Lauderdale, Florida (1994)"},{"key":"203_CR20","doi-asserted-by":"crossref","unstructured":"Stern, U., Dill, D.L.: Parallelizing the Murphi Verifier. In: Presented at Computer-Aided Verification (1997)","DOI":"10.1007\/3-540-63166-6_26"},{"key":"203_CR21","doi-asserted-by":"crossref","unstructured":"Heyman, T., Geist, D., Grumberg, O., Schuster, A.: Achieving scalability in parallel reachability analysis of very large circuits. In: Presented at Computer-Aided Verification (2000)","DOI":"10.1007\/10722167_6"},{"key":"203_CR22","doi-asserted-by":"crossref","unstructured":"Narayan, A., Isles, A., Jain, J., Brayton, R., Sangiovanni-Vincentelli, A.L.: Reachability analysis using partitioned-ROBDDs. In: Presented at International Conference on Computer-Aided Design (1997)","DOI":"10.1109\/ICCAD.1997.643565"},{"key":"203_CR23","unstructured":"Yadgar, A.: Parallel SAT solving for model checking. ww.cs.technion.ac.il\/\u223cyadgar\/Research\/research.pdf (2002)"},{"key":"203_CR24","doi-asserted-by":"crossref","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. Commun. ACM 5, 394\u2013397 (1962)","journal-title":"Commun. ACM."},{"key":"203_CR25","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Proceedings of Workshop on Tools and Algorithms for Analysis and Construction of Systems (TACAS), LNCS, vol. 1579 (1999)","DOI":"10.21236\/ADA360973"},{"key":"203_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":"203_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 Res. Dev. 44(1), 60\u201363 (2003)","journal-title":"NEC Res. Dev."}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-005-0203-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-005-0203-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-005-0203-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T03:25:21Z","timestamp":1559100321000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-005-0203-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,4,5]]},"references-count":27,"journal-issue":{"issue":"4-5","published-print":{"date-parts":[[2006,8]]}},"alternative-id":["203"],"URL":"https:\/\/doi.org\/10.1007\/s10009-005-0203-z","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,4,5]]}}}