{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T08:47:54Z","timestamp":1725612474413},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540326045"},{"type":"electronic","value":"9783540326052"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11678779_5","type":"book-chapter","created":{"date-parts":[[2006,3,2]],"date-time":"2006-03-02T13:03:26Z","timestamp":1141304606000},"page":"56-75","source":"Crossref","is-referenced-by-count":10,"title":["Simultaneous SAT-Based Model Checking of Safety Properties"],"prefix":"10.1007","author":[{"given":"Zurab","family":"Khasidashvili","sequence":"first","affiliation":[]},{"given":"Alexander","family":"Nadel","sequence":"additional","affiliation":[]},{"given":"Amit","family":"Palti","sequence":"additional","affiliation":[]},{"given":"Ziyad","family":"Hanna","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","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.) TACAS 1999. LNCS, vol.\u00a01579, p. 193. Springer, Heidelberg (1999)"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Strichman, O., Zhu, Y.: Bounded Model Checking. Chapter in Advances in Computers\u00a058 (2003)","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Trans. Computers\u00a0C-35(8) (1986)","DOI":"10.1109\/TC.1986.1676819"},{"key":"5_CR4","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM\u00a0(5), 394\u2013397 (1962)","DOI":"10.1145\/368273.368557"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. J. ACM\u00a07 (1960)","DOI":"10.1145\/321033.321034"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: Temporal induction by incremental SAT solving. In: International Workshop on Bounded Model Checking, BMC 2003 (2003)","DOI":"10.1016\/S1571-0661(05)82542-3"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Fraer, R., Ikram, S., Kamhi, G., Leonard, T., Mokkedem, A.: Accelerated verification of RTL assertions based on satisfiability solvers, HLDVT (2002)","DOI":"10.1109\/HLDVT.2002.1224437"},{"key":"5_CR9","unstructured":"Goldberg, E., Novikov, Y.: An efficient learning procedure for multiple implication check. In: Design, Automation, and Test in Europe, DATE 2001 (2001)"},{"key":"5_CR10","unstructured":"Gomes, C.P., Selman, B., Kautz, H.: Boosting combinatorial search through randomization. In: National Conference on Artificial Intelligence (1998)"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Kuehlmann, A., Ganai, M.K., Paruthi, V.: Circuit-based Boolean reasoning. In: DAC (2001)","DOI":"10.1145\/378239.378470"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Khasidashvili, Z., Skaba, M., Kaiss, D., Hanna, Z.: Theoretical framework for compositional sequential hardware equivalence verification in presence of design constraints. In: ICCAD 2004 (2004)","DOI":"10.1109\/ICCAD.2004.1382543"},{"key":"5_CR13","unstructured":"Lynce, I., Marques-Silva, J.: Building state-of-the-art SAT solvers. In: European Conference on Artificial Intelligence, ECAI (2002)"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Marques Silva, J.P., Sakallah, K.A.: Robust search algorithm for test pattern generation. In: IEEE Fault-Tolerant Computing Symposium (1997)","DOI":"10.1109\/FTCS.1997.614088"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers\u00a048 (1999)","DOI":"10.1109\/12.769433"},{"key":"5_CR16","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer, Dordrecht (1993)"},{"key":"5_CR17","unstructured":"Nadel, A.: Backtrack search algorithms for propositional satisfiability: Review and Innovations, Master Thesis, the Hebrew University of Jerusalem (2002)"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Prasad, M., Biere, A., Gupta, A.: A survey of recent advances in SAT-based formal verification. Int. Journal on Software Tools for Technology Transfer (STTT)\u00a07(2) (2005)","DOI":"10.1007\/s10009-004-0183-4"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/3-540-40922-X_8","volume-title":"Formal Methods in Computer-Aided Design","author":"M. Sheeran","year":"2000","unstructured":"Sheeran, M., Singh, S., Stalmarck, G.: Checking safety properties using induction and a SAT-solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 108\u2013125. Springer, Heidelberg (2000)"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Strichman, O.: Accelerating bounded model checking of safety properties. Formal Methods in System Design\u00a024 (2004)","DOI":"10.1023\/B:FORM.0000004785.67232.f8"},{"key":"5_CR21","unstructured":"Zabih, R., McAllester, D.A.: A rearrangement search strategy for determining propositional satisfiability. In: National Conference on Artificial Intelligence (1988)"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"Zhang, L., Madigan, C.F., Moskewicz, M.H., Malik, S.: Efficient conflict driven learning in a boolean satisfiability solver. In: International Conference on Computer Aided Design, ICCAD 2001 (2001)","DOI":"10.1145\/774572.774637"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"Whittemore, J., Kim, K., Sakallah, K.: SATIRE: A new incremental satisfiability engine. In: DAC (2001)","DOI":"10.1145\/378239.379019"}],"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\/11678779_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:15:40Z","timestamp":1619507740000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11678779_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540326045","9783540326052"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/11678779_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}