{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T04:53:25Z","timestamp":1725512005030},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540709510"},{"type":"electronic","value":"9783540709527"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-70952-7_21","type":"book-chapter","created":{"date-parts":[[2007,6,26]],"date-time":"2007-06-26T08:40:01Z","timestamp":1182847201000},"page":"301-315","source":"Crossref","is-referenced-by-count":6,"title":["Parallel SAT Solving in Bounded Model Checking"],"prefix":"10.1007","author":[{"given":"Erika","family":"\u00c1brah\u00e1m","sequence":"first","affiliation":[]},{"given":"Tobias","family":"Schubert","sequence":"additional","affiliation":[]},{"given":"Bernd","family":"Becker","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Fr\u00e4nzle","sequence":"additional","affiliation":[]},{"given":"Christian","family":"Herde","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"21_CR1","unstructured":"AVACS: Automatic Verification and Analysis of Complex Systems. \n                    \n                      http:\/\/www.avacs.org"},{"key":"21_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"396","DOI":"10.1007\/978-3-540-30579-8_26","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"E. \u00c1brah\u00e1m","year":"2005","unstructured":"\u00c1brah\u00e1m, E., Becker, B., Klaedke, F., Steffen, M.: Optimizing bounded model checking for linear hybrid systems. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 396\u2013412. Springer, Heidelberg (2005)"},{"key":"21_CR3","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R. Alur","year":"1995","unstructured":"Alur, R., Courcoubetis, C., Henzinger, T., Ho, P., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical Computer Science\u00a0138, 3\u201334 (1995)","journal-title":"Theoretical Computer Science"},{"key":"21_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","year":"2004","unstructured":"Alur, R., Peled, D.A. (eds.): CAV 2004. LNCS, vol.\u00a03114. Springer, Heidelberg (2004)"},{"key":"21_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/3-540-45620-1_17","volume-title":"Automated Deduction - CADE-18","author":"G. Audemard","year":"2002","unstructured":"Audemard, G., Bertoli, P., Cimatti, A., Korni\u0142owicz, A., Sebastiani, R.: A SAT based approach for solving formulas over boolean and linear mathematical propositions. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, p. 195. Springer, Heidelberg (2002)"},{"key":"21_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"515","DOI":"10.1007\/978-3-540-27813-9_49","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2004","unstructured":"Barrett, C., Berezin, S.: CVC Lite: A new implementation of the cooperating validity checker category B. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 515\u2013518. Springer, Heidelberg (2004)"},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/3-540-45657-0_18","volume-title":"Computer Aided Verification","author":"C.W. Barrett","year":"2002","unstructured":"Barrett, C.W., Dill, D.L., Stump, A.: Checking satisfiability of first-order formulas by incremental translation to SAT. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 236. Springer, Heidelberg (2002)"},{"key":"21_CR8","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., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"issue":"3\u20134","key":"21_CR9","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/BF02127976","volume":"17","author":"M. B\u00f6hm","year":"1996","unstructured":"B\u00f6hm, M., Speckenmeyer, E.: A Fast Parallel SAT-Solver \u2013 Efficient Workload Balancing. Annals of Mathematics and Artificial Intelligence\u00a017(3\u20134), 381\u2013400 (1996)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"21_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1007\/978-3-540-27813-9_13","volume-title":"Computer Aided Verification","author":"L. Moura de","year":"2004","unstructured":"de Moura, L., Rue\u00df, H.: An experimental evaluation of ground decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 162\u2013174. Springer, Heidelberg (2004)"},{"key":"21_CR11","unstructured":"de Moura, L., Rue\u00df, H., Rushby, J., Shankar, N.: Embedded deduction with ICS. In: Martin, B. (ed.) Proc. of HCSS\u201903 (2003)"},{"key":"21_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1007\/978-3-540-45069-6_2","volume-title":"Computer Aided Verification","author":"L. Moura de","year":"2003","unstructured":"de Moura, L., Rue\u00df, H., Sorea, M.: Bounded model checking and induction: From refutation to verification. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 14\u201326. Springer, Heidelberg (2003)"},{"key":"21_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 502\u2013518. Springer, Heidelberg (2004)"},{"key":"21_CR14","first-page":"119","volume":"133","author":"M. Fr\u00e4nzle","year":"2005","unstructured":"Fr\u00e4nzle, M., Herde, C.: Efficient proof engines for bounded model checking of hybrid systems. ENTCS\u00a0133, 119\u2013137 (2005)","journal-title":"ENTCS"},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: BerkMin: A Fast and Robust SAT-Solver. In: Proc. of DATE\u201902, pp. 142\u2013149 (2002)","DOI":"10.1109\/DATE.2002.998262"},{"key":"21_CR16","doi-asserted-by":"crossref","unstructured":"Groote, J.F., Koorn, J.W.C., van Vlijmen, S.F.M.: The safety guaranteeing system at station Hoorn-Kersenboogerd. In: Proc. of Compass\u201995, pp. 57\u201368. National Institute of Standards and Technology (1995)","DOI":"10.1109\/CMPASS.1995.521887"},{"issue":"6","key":"21_CR17","doi-asserted-by":"publisher","first-page":"789","DOI":"10.1016\/0167-8191(96)00024-5","volume":"22","author":"W. Gropp","year":"1996","unstructured":"Gropp, W., Lusk, E., Doss, N., Skjellum, A.: A high-performance, portable implementation of the MPI message passing interface standard. Parallel Computing\u00a022(6), 789\u2013828 (1996)","journal-title":"Parallel Computing"},{"key":"21_CR18","first-page":"278","volume-title":"Proc. of LICS\u201996","author":"T. Henzinger","year":"1996","unstructured":"Henzinger, T.: The theory of hybrid automata. In: Proc. of LICS\u201996, pp. 278\u2013292. IEEE Computer Society Press, Los Alamitos (1996)"},{"key":"21_CR19","series-title":"Electronic Notes in Computer Science","volume-title":"Proc. of PDMC\u201904","author":"F. Holm\u00e9n","year":"2004","unstructured":"Holm\u00e9n, F., Leucker, M., Lindstr\u00f6m, M.: UppDMC \u2013 a distributed model checker for fragments of the \u03bc-calculus. In: Brim, L., Leucker, M. (eds.) Proc. of PDMC\u201904. Electronic Notes in Computer Science, vol.\u00a0128\/3, Elsevier Science Publishers, Amsterdam (2004)"},{"key":"21_CR20","doi-asserted-by":"crossref","unstructured":"Lewis, M., Schubert, T., Becker, B.: Speedup Techniques Utilized in Modern SAT Solvers \u2013 An Analysis in the MIRA Environment. In: 8th International Conference on Theory and Applications of Satisfiability Testing (2005)","DOI":"10.1007\/11499107_36"},{"key":"21_CR21","volume-title":"Distributed Algorithms","author":"N. Lynch","year":"1996","unstructured":"Lynch, N.: Distributed Algorithms. Kaufman Publishers, San Francisco (1996)"},{"issue":"5","key":"21_CR22","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"J. Marques-Silva","year":"1999","unstructured":"Marques-Silva, J., Sakallah, K.: GRASP: A Search Algorithm for Propositional Satisfiability. IEEE Transactions on Computers\u00a048(5), 506\u2013521 (1999)","journal-title":"IEEE Transactions on Computers"},{"key":"21_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/11691617_7","volume-title":"Model Checking Software","author":"I. Melatti","year":"2006","unstructured":"Melatti, I., Palmer, R., Sawaya, G., Yang, Y., Kirby, R.M., Gopalakrishnan, G.: Parallel and distributed model checking in Eddy. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol.\u00a03925, pp. 108\u2013125. Springer, Heidelberg (2006)"},{"key":"21_CR24","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Yang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proc. of DAC\u201901, pp. 530\u2013535 (2001)","DOI":"10.1145\/378239.379017"},{"key":"21_CR25","doi-asserted-by":"crossref","unstructured":"Schubert, T., Lewis, M., Becker, B.: PaMira \u2013 a Parallel SAT Solver with Knowledge Sharing. In: 6th International Workshop on Microprocessor Test and Verification (2005)","DOI":"10.1109\/MTV.2005.17"},{"issue":"1","key":"21_CR26","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1023\/B:FORM.0000004785.67232.f8","volume":"24","author":"O. Shtrichman","year":"2004","unstructured":"Shtrichman, O.: Accelerating bounded model checking of safety formulas. Formal Methods in System Design\u00a024(1), 5\u201324 (2004)","journal-title":"Formal Methods in System Design"},{"key":"21_CR27","doi-asserted-by":"crossref","unstructured":"Sinz, C., Blochinger, W., K\u00fcchlin, W.: PaSAT \u2013 Parallel SAT-Checking with Lemma Exchange: Implementation and Applications. In: Proc. of LICS\u201901 (2001)","DOI":"10.1016\/S1571-0653(04)00323-3"},{"key":"21_CR28","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"The VIS Group","year":"1996","unstructured":"The VIS Group: VIS: A system for verification and synthesis. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, Springer, Heidelberg (1996)"},{"key":"21_CR29","unstructured":"Torrisi, F.D.: Modeling and Reach-Set Computation for Analysis and Optimal Control of Discrete Hybrid Automata. Doctoral dissertation, ETH Z\u00fcrich (2003)"},{"key":"21_CR30","unstructured":"Tseitin, G.: On the complexity of derivations in propositional calculus. In: Studies in Constructive Mathematics and Mathematical Logics (1968)"},{"key":"21_CR31","unstructured":"VIS Benchmark Suite. \n                    \n                      http:\/\/vlsi.colorado.edu\/~vis"},{"key":"21_CR32","unstructured":"Wolfman, S.A., Weld, D.S.: The LPSAT engine & its application to resource planning. In: Dean, T. (ed.) Proc. of 16th International Joint Conference on Artificial Intelligence, pp. 310\u2013315 (1999)"},{"key":"21_CR33","volume-title":"IEEE\/ACM International Conference on Computer-Aided Design","author":"L. Zhang","year":"2001","unstructured":"Zhang, L., Madigan, C., Moskewicz, M., Malik, S.: Efficient Conflict Driven Learning in a Boolean Satisfiability Solver. In: IEEE\/ACM International Conference on Computer-Aided Design, ACM Press, New York (2001)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods: Applications and Technology"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-70952-7_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,17]],"date-time":"2019-02-17T08:35:20Z","timestamp":1550392520000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-70952-7_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540709510","9783540709527"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-70952-7_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}