{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:58:17Z","timestamp":1725494297271},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540755951"},{"type":"electronic","value":"9783540755968"}],"license":[{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-75596-8_32","type":"book-chapter","created":{"date-parts":[[2007,11,3]],"date-time":"2007-11-03T10:03:37Z","timestamp":1194084217000},"page":"457-473","source":"Crossref","is-referenced-by-count":12,"title":["3-Valued Circuit SAT for STE with Automatic Refinement"],"prefix":"10.1007","author":[{"given":"Orna","family":"Grumberg","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Assaf","family":"Schuster","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Avi","family":"Yadgar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"32_CR1","volume-title":"DAC","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Fujita, M., Zhu, Y.: Symbolic model checking using SAT procedures instead of BDDs. In: DAC, IEEE Computer Society Press, Los Alamitos (1999)"},{"key":"32_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"454","DOI":"10.1007\/3-540-44585-4_44","volume-title":"CAV 2001","author":"P. Bjesse","year":"2001","unstructured":"Bjesse, P., Leonard, T., Mokkedem, A.: Finding bugs in an alpha microprocessor using satisfiability solvers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 454\u2013464. Springer, Heidelberg (2001)"},{"issue":"5","key":"32_CR3","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E.M. Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. Journal of the ACM\u00a050(5), 752\u2013794 (2003)","journal-title":"Journal of the ACM"},{"key":"32_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"CHARME 2005","author":"K. Classen","year":"2005","unstructured":"Classen, K., Roorda, J.-W.: A new SAT-based algorithm for symbolic trajectory evaluation. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol.\u00a03725, Springer, Heidelberg (2005)"},{"key":"32_CR5","doi-asserted-by":"crossref","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. CACM\u00a05(7) (July 1962)","DOI":"10.1145\/368273.368557"},{"issue":"3","key":"32_CR6","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. JACM\u00a07(3), 201\u2013215 (1960)","journal-title":"JACM"},{"issue":"12","key":"32_CR7","doi-asserted-by":"publisher","first-page":"1137","DOI":"10.1109\/TC.1983.1676174","volume":"32","author":"H. Fujiwara","year":"1983","unstructured":"Fujiwara, H., Shimono, T.: On the acceleration of test generation algorithms. IEEE Trans. Computers\u00a032(12), 1137\u20131144 (1983)","journal-title":"IEEE Trans. Computers"},{"key":"32_CR8","doi-asserted-by":"crossref","unstructured":"Ganai, M.K., Ashar, P., Gupta, A., Zhang, L., Malik, S.: Combining Strengths of Circuit-Based and CNF-Based Algorithms for a High-Performance SAT Solver. In: DAC (2002)","DOI":"10.1145\/514100.514105"},{"key":"32_CR9","unstructured":"Grumberg, O., Schuster, A., Yadgar, A.: Hybrid BDD and all-sat method for model checking and other application. Technical report, Technion, CS-2007-08\u00a0 (2007)"},{"key":"32_CR10","series-title":"Lecture Notes in Computer Science","volume-title":"CAV 2004","author":"H. Jin","year":"2004","unstructured":"Jin, H., Awedh, M., Somenzi, F.: CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, Springer, Heidelberg (2004)"},{"key":"32_CR11","first-page":"10892","volume-title":"DATE 2003","author":"F. Lu","year":"2003","unstructured":"Lu, F., Wang, L.C., Cheng, K.-T., Huang, R.C.Y.: A Circuit SAT Solver With Signal Correlation Guided Learning. In: DATE 2003, p. 10892. IEEE Computer Society Press, Washington (2003)"},{"key":"32_CR12","unstructured":"Marques-Silva, J.P., Sakallah, K.A.: Conflict analysis in search algorithms for propositional satisfiability. In: IEEE ICTAI (1996)"},{"key":"32_CR13","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: DAC 2001. 39th Design Aotomation Conference (2001)","DOI":"10.1145\/378239.379017"},{"key":"32_CR14","doi-asserted-by":"crossref","unstructured":"Pandey, M., Raimi, R., Bryant, R.E., Abadir, M.S.: Formal verification of content addressable memories using symbolic trajectory evaluation. dac, 00, 167 (1997)","DOI":"10.1145\/266021.266056"},{"key":"32_CR15","unstructured":"Roorda, J.-W.: Symbolic trajectory evaluation using a satisfiability solver. Licentiate Thesis (2005)"},{"key":"32_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/11817963_19","volume-title":"CAV 2006","author":"J.-W. Roorda","year":"2006","unstructured":"Roorda, J.-W., Claessen, K.: Sat-based assistance in abstraction refinement for symbolic trajectory evaluation. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 175\u2013189. Springer, Heidelberg (2006)"},{"key":"32_CR17","doi-asserted-by":"crossref","unstructured":"Schubert, T.: High level formal verification of next-generation microprocessors. In: DAC (2003)","DOI":"10.1145\/775833.775834"},{"key":"32_CR18","doi-asserted-by":"crossref","unstructured":"Seger, C.-J.H., Bryant, R.E.: Formal verification by symbolic evaluation of partially-ordered trajectories. Formal Methods in System Design\u00a06(2) (1995)","DOI":"10.1007\/BF01383966"},{"key":"32_CR19","doi-asserted-by":"crossref","unstructured":"Seger, C.-J.H., Jones, R.B., O\u2019Leary, J.W., Melham, T.F., Aagaard, M., Barrett, C., Syme, D.: An industrially effective environment for formal hardware verification. IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems\u00a024(9) (2005)","DOI":"10.1109\/TCAD.2005.850814"},{"key":"32_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"190","DOI":"10.1007\/11817963_20","volume-title":"CAV 2006","author":"R. Tzoref","year":"2006","unstructured":"Tzoref, R., Grumberg, O.: Automatic refinement and vacuity detection for symbolic trajectory evaluation. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 190\u2013204. Springer, Heidelberg (2006)"},{"key":"32_CR21","unstructured":"Yang, J., Gil, R., Singerman, E.: satGSTE: Combining the abstraction of GSTE with the capacity of a SAT solver. In: DCC (2004)"},{"key":"32_CR22","doi-asserted-by":"crossref","unstructured":"Yang, J., Goel, A.: GSTE through a case study. In: ICCAD (2002)","DOI":"10.1145\/774572.774651"},{"key":"32_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030077","volume-title":"CADE 1997","author":"H. Zhang","year":"1997","unstructured":"Zhang, H.: SATO: An efficient propositional prover. In: McCune, W. (ed.) CADE 1997. LNCS, vol.\u00a01249, Springer, Heidelberg (1997)"},{"key":"32_CR24","doi-asserted-by":"crossref","unstructured":"Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient conflict driven learning in boolean satisfiability solver. In: ICCAD (2001)","DOI":"10.1145\/774572.774637"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-75596-8_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T10:51:06Z","timestamp":1558263066000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-75596-8_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540755951","9783540755968"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-75596-8_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2007]]}}}