{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,10]],"date-time":"2025-12-10T08:29:05Z","timestamp":1765355345060,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":78,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540343042"},{"type":"electronic","value":"9783540343059"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11757283_5","type":"book-chapter","created":{"date-parts":[[2006,11,27]],"date-time":"2006-11-27T13:02:12Z","timestamp":1164632532000},"page":"108-143","source":"Crossref","is-referenced-by-count":26,"title":["SAT-Based Verification Methods and Applications in Hardware Verification"],"prefix":"10.1007","author":[{"given":"Aarti","family":"Gupta","sequence":"first","affiliation":[]},{"given":"Malay K.","family":"Ganai","sequence":"additional","affiliation":[]},{"given":"Chao","family":"Wang","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"issue":"4","key":"5_CR2","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1109\/43.275352","volume":"13","author":"R. Burch","year":"1994","unstructured":"Burch, R., Clarke, E.M., Long, D.E., McMillan, K.L., Dill, D.: Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems\u00a013(4), 401\u2013424 (1994)","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"5_CR3","doi-asserted-by":"publisher","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":"5_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":"5_CR5","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":"5_CR6","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":"5_CR7","doi-asserted-by":"crossref","unstructured":"Zhang, H.: SATO: An efficient propositional prover. In: Proceedings of International Conference on Automated Deduction, pp. 272\u2013275 (1997)","DOI":"10.1007\/3-540-63104-6_28"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Goldberg, E., Novikov, Y.: BerkMin: A Fast and Robust SAT-Solver. In: Proceedings of Conference on Design Automation & Test Europe (DATE), pp. 142\u2013149 (2002)","DOI":"10.1109\/DATE.2002.998262"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/3-540-45657-0_2","volume-title":"Computer Aided Verification","author":"L. Zhang","year":"2002","unstructured":"Zhang, L., Malik, S.: The Quest for Efficient Boolean Satisfiability Solvers. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 17\u201336. Springer, Heidelberg (2002)"},{"issue":"2","key":"5_CR10","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/s10009-004-0183-4","volume":"7","author":"M. Prasad","year":"2005","unstructured":"Prasad, M., Biere, A., Gupta, A.: A survey of recent advances in SAT-based formal verification. Software Tools for Technology Transfer\u00a07(2), 156\u2013173 (2005)","journal-title":"Software Tools for Technology Transfer"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Lu, F., Wang, L.-C., Cheng, K.-T., Moondanos, J., Hanna, Z.: A signal correlation guided ATPG solver and its applications for solving difficult industrial cases. In: Proceedings of the Design Automation Conference, pp. 436\u2013441 (2003)","DOI":"10.1145\/775832.775947"},{"key":"5_CR12","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_CR13","doi-asserted-by":"crossref","unstructured":"Gupta, A., Ganai, M., Wang, C., Yang, Z., Ashar, P.: Learning from BDDs in SAT-based bounded model checking. In: Design Automation Conference (2003)","DOI":"10.1145\/776038.776040"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-540-39724-3_30","volume-title":"Correct Hardware Design and Verification Methods","author":"M.K. Ganai","year":"2003","unstructured":"Ganai, M.K., Gupta, A., Yang, Z.-J., Ashar, P.: Efficient distributed SAT and SAT-based distributed bounded model checking. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 334\u2013347. Springer, Heidelberg (2003)"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Ganai, M., Gupta, A., Ashar, P.: Beyond safety: Customized SAT-based model checking. In: Proceedings of the Design Automation Conference, pp. 738\u2013743 (2005)","DOI":"10.1145\/1065579.1065773"},{"key":"5_CR16","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., St\u00e5lmarck, 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_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"206","DOI":"10.1007\/978-3-540-45069-6_20","volume-title":"Computer Aided Verification","author":"A. Gupta","year":"2003","unstructured":"Gupta, A., Ganai, M.K., Wang, C., Yang, Z.-J., Ashar, P.: Abstraction and BDDs complement SAT-based BMC in diVer. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 206\u2013209. Springer, Heidelberg (2003)"},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/3-540-40922-X_22","volume-title":"Formal Methods in Computer-Aided Design","author":"A. Gupta","year":"2000","unstructured":"Gupta, A., Yang, Z.-J., Ashar, P., Gupta, A.: SAT-based image computation with application in reachability analysis. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 354\u2013371. Springer, Heidelberg (2000)"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Gupta, A., Yang, Z., Ashar, P.: Dynamic detection and removal of inactive clauses in SAT with application in image computation. In: Proceedings of Design Automation Conference (2001)","DOI":"10.1145\/378239.379018"},{"key":"5_CR20","unstructured":"Gupta, A., Yang, Z., Ashar, P., Zhang, L., Malik, S.: Partition-Based Decision Heuristics for Image Computation using SAT and BDDs. In: Proceedings of International Conference on Computer-Aided Design (2001)"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Ganai, M., Gupta, A., Ashar, P.: Efficient SAT-based unbounded symbolic model checking using circuit cofactoring. In: Proceedings of the International Conference on Computer-Aided Design, pp. 510\u2013517 (2004)","DOI":"10.1109\/ICCAD.2004.1382631"},{"key":"5_CR22","unstructured":"Gupta, A., Ganai, M., Yang, J., Ashar, P.: Iterative Abstraction using SAT-based BMC with Proof Analysis. In: Proceedings of International Conference on Computer Aided Design (ICCAD) (2003)"},{"key":"5_CR23","unstructured":"Gupta, A., Ganai, M., Ashar, P.: Lazy constraints and SAT heuristics for proof-based abstraction. In: Proceedings of the International Conference on VLSI Design, pp. 183\u2013188 (2005)"},{"key":"5_CR24","unstructured":"Ganai, M., Kuehlmann, A.: On-the-fly compression of logical circuits. In: Proceedings of International Workshop on Logic Synthesis (2000)"},{"key":"5_CR25","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\/514100.514105"},{"key":"5_CR26","volume-title":"Digital Systems Testing and Testable Design","author":"M. Abramovici","year":"1990","unstructured":"Abramovici, M., Breuer, M.A., Friedman, A.D.: Digital Systems Testing and Testable Design. Computer Science Press, Rockville (1990)"},{"key":"5_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/978-3-540-27813-9_34","volume-title":"Computer Aided Verification","author":"M.K. Ganai","year":"2004","unstructured":"Ganai, M.K., Gupta, A., Ashar, P.: Efficient modeling of embedded memories in bounded model checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 440\u2013452. Springer, Heidelberg (2004)"},{"key":"5_CR28","doi-asserted-by":"crossref","unstructured":"Ganai, M., Gupta, A., Ashar, P.: Verification of embedded memory systems using efficient memory modeling. In: Proceedings of Design Automation and Test Europe (DATE), pp. 1096\u20131101 (2005)","DOI":"10.1109\/DATE.2005.325"},{"key":"5_CR29","doi-asserted-by":"publisher","first-page":"575","DOI":"10.1007\/978-3-540-31980-1_41","volume-title":"Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"M. Ganai","year":"2005","unstructured":"Ganai, M., Gupta, A., Ashar, P.: DiVer: SAT-based model checking platform for verifying large scale systems. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp. 575\u2013580. Springer, Heidelberg (2005)"},{"key":"5_CR30","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-1-4615-3966-7_6","volume-title":"High Level VLSI Synthesis","author":"K. Wakabayashi","year":"1991","unstructured":"Wakabayashi, K.: Cyber: High level synthesis system from software into ASIC. In: Camposano, R., Wolf, W. (eds.) High Level VLSI Synthesis, pp. 127\u2013151. Kluwer Academic Publishers, Dordrecht (1991)"},{"key":"5_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/11513988_31","volume-title":"Computer Aided Verification","author":"F. Ivan\u010di\u0107","year":"2005","unstructured":"Ivan\u010di\u0107, F., Yang, Z., Ganai, M.K., Gupta, A., Shlyakhter, I., Ashar, P.: F-Soft: Software Verification Platform. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 301\u2013306. Springer, Heidelberg (2005)"},{"key":"5_CR32","doi-asserted-by":"crossref","unstructured":"Ivancic, F., Shlyakhter, I., Gupta, A., Ganai, M., Kahlon, V., Wang, C., Yang, Z.: Model checking C programs using F-Soft. In: Proceedings of the International Conference on Computer Design, pp. 297\u2013308 (2005)","DOI":"10.1109\/ICCD.2005.77"},{"key":"5_CR33","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, pp. 236\u2013249. Springer, Heidelberg (2002)"},{"key":"5_CR34","doi-asserted-by":"crossref","unstructured":"Seshia, S., Lahiri, S., Bryant, R.E.: A hybrid SAT-based decision procedure for separation logic with uninterpreted functions. In: Design Automation Conference (2003)","DOI":"10.1145\/775944.775945"},{"key":"5_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1007\/11591191_23","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C. Wang","year":"2005","unstructured":"Wang, C., Ivan\u010di\u0107, F., Ganai, M.K., Gupta, A.: Deciding separation logic formulae by SAT and incremental negative cycle elimination. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS, vol.\u00a03835, pp. 322\u2013336. Springer, Heidelberg (2005)"},{"key":"5_CR36","doi-asserted-by":"crossref","unstructured":"Ganai, M., Talupur, M., Gupta, A.: SDSAT: Tight integration of small domain encoding and lazy approaches in a separation logic solver. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (2006)","DOI":"10.1007\/11691372_9"},{"key":"5_CR37","volume-title":"Computers and Intractability: A guide to the theory of NP-Completeness","author":"M.R. Garey","year":"1979","unstructured":"Garey, M.R., Johnson, D.S.: Computers and Intractability: A guide to the theory of NP-Completeness. W.H. Freeman and Co., New York (1979)"},{"issue":"1","key":"5_CR38","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1109\/43.108614","volume":"11","author":"T. Larrabee","year":"1992","unstructured":"Larrabee, T.: Test pattern generation using Boolean Satisfiability. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems\u00a011(1), 4\u201315 (1992)","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"5_CR39","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":"5_CR40","unstructured":"Zhang, L., Malik, S.: Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications. In: Proceedings of Conference on Design Automation & Test Europe (DATE) (2003)"},{"key":"5_CR41","unstructured":"Goldberg, E., Novikov, Y.: Verification of Proofs of Unsatisfiability for CNF Formulas. In: Proceedings of Conference on Design Automation & Test Europe (DATE) (2003)"},{"key":"5_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-36577-X_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L., Amla, N.: Automatic Abstraction without Counterexamples. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 2\u201317. Springer, Heidelberg (2003)"},{"issue":"12","key":"5_CR43","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1109\/TC.1983.1676174","volume":"C-32","author":"H. Fujiwara","year":"1983","unstructured":"Fujiwara, H., Shimono, T.: On the Acceleration of Test Generation Algorithms. IEEE Transactions on Computers\u00a0C-32(12), 265\u2013272 (1983)","journal-title":"IEEE Transactions on Computers"},{"issue":"3","key":"5_CR44","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1109\/TC.1981.1675757","volume":"C-30","author":"P. Goel","year":"1981","unstructured":"Goel, P.: An implicit enumeration algorithm to generate tests for Combinational circuits. IEEE Transactions on Computers\u00a0C-30(3), 215\u2013222 (1981)","journal-title":"IEEE Transactions on Computers"},{"key":"5_CR45","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"},{"issue":"12","key":"5_CR46","doi-asserted-by":"publisher","first-page":"1377","DOI":"10.1109\/TCAD.2002.804386","volume":"21","author":"A. Kuehlmann","year":"2002","unstructured":"Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.: Robust Boolean Reasoning for Equivalence Checking and Functional Property Verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems\u00a021(12), 1377\u20131394 (2002)","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"5_CR47","doi-asserted-by":"crossref","unstructured":"Iyer, M., Parthasarthy, G., Cheng, K.-T.: SATORI \u2013 A fast sequential SAT engine for circuits. In: Proceedings of the International Conference on Computer-Aided Design, pp. 320\u2013325 (2003)","DOI":"10.1109\/ICCAD.2003.159706"},{"key":"5_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/978-3-540-27813-9_50","volume-title":"Computer Aided Verification","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, pp. 519\u2013522. Springer, Heidelberg (2004)"},{"issue":"5","key":"5_CR49","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The Model Checker SPIN. IEEE Transactions of Software Engineering\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Transactions of Software Engineering"},{"key":"5_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/3-540-36384-X_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"D. Kr\u00f6ning","year":"2002","unstructured":"Kr\u00f6ning, D., Strichman, O.: Efficient Computation of Recurrence Diameters. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol.\u00a02575, pp. 298\u2013309. Springer, Heidelberg (2002)"},{"key":"5_CR51","doi-asserted-by":"crossref","unstructured":"Shtrichman, O.: Tuning SAT Checkers for Bounded Model Checking. In: Proceedings of International Conference on Computer-Aided Verification (2000)","DOI":"10.1007\/10722167_36"},{"key":"5_CR52","doi-asserted-by":"crossref","unstructured":"Shtrichman, O.: Pruning Techniques for the SAT-based bounded model checking. In: Proceedings of Workshop on Tools and Algorithms for the Analysis and Construction of Systems (TACAS) (2001)","DOI":"10.1007\/3-540-44798-9_4"},{"key":"5_CR53","volume-title":"Proceedings of the First International Workshop on Bounded Model Checking (BMC)","author":"N. Een","year":"2003","unstructured":"Een, N., Sorensson, N.: Temporal induction by incremental SAT solving. In: Proceedings of the First International Workshop on Bounded Model Checking (BMC). Elsevier, Amsterdam (2003)"},{"key":"5_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/3-540-45657-0_12","volume-title":"Computer Aided Verification","author":"J. Baumgartner","year":"2002","unstructured":"Baumgartner, J., Kuehlmann, A., Abraham, J.A.: Property Checking via Structural Analysis. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 151. Springer, Heidelberg (2002)"},{"key":"5_CR55","doi-asserted-by":"crossref","unstructured":"Mneimneh, M., Sakallah, K.: SAT-based sequential depth computation. In: Proceedings of the First International Workshop on Constraints in Formal Verification (2002)","DOI":"10.1145\/1119772.1119790"},{"key":"5_CR56","doi-asserted-by":"crossref","unstructured":"Kuehlmann, A., Krohm, F.: Equivalence Checking using Cuts and Heaps. In: Proceedings of Design Automation Conference (1997)","DOI":"10.1145\/266021.266090"},{"key":"5_CR57","doi-asserted-by":"crossref","unstructured":"Whittemore, J., Kim, J., Sakallah, K.: SATIRE: A new incremental SAT engine. In: Proceedings of the Design Automation Conference (2001)","DOI":"10.1145\/378239.379019"},{"key":"5_CR58","unstructured":"Ganai, M., Aziz, A.: Improved SAT-based Bounded Reachability Analysis. In: Proceedings of VLSI Design Conference (2002)"},{"key":"5_CR59","unstructured":"Brayton, R., Somenzi, F., et al.: VIS: Verification Interacting with Synthesis (2002), http:\/\/vlsi.colorado.edu\/~vis"},{"key":"5_CR60","doi-asserted-by":"crossref","unstructured":"Cabodi, S.N., Quer, S.: Improving SAT-based bounded model checking by means of BDD-based approximate traversals. In: Proceedings of Design Automation and Test Europe, pp. 898\u2013903 (2003)","DOI":"10.1109\/DATE.2003.1253720"},{"key":"5_CR61","volume-title":"Computer-Aided Verification of Co-ordinating Processes: The Automata-Theoretic Approach","author":"R.P. Kurshan","year":"1994","unstructured":"Kurshan, R.P.: Computer-Aided Verification of Co-ordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton (1994)"},{"key":"5_CR62","volume-title":"Electrical Engineering","author":"Y. Zhao","year":"2001","unstructured":"Zhao, Y.: Accelerating Boolean Satisfiability through Application Specific Processing. In: Electrical Engineering, Princeton University, Princeton (2001)"},{"key":"5_CR63","doi-asserted-by":"crossref","unstructured":"Burch, J.R., Dill, D.: Automatic verification of pipelined microprocessor control. In: Proceedings of the International Conference on Computer Aided Verification (1994)","DOI":"10.1007\/3-540-58179-0_44"},{"key":"5_CR64","unstructured":"Bryant, R.E., German, S., Velev, M.N.: Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic. In: Proceedings of the International Conference on Computer Aided Verification (1999)"},{"key":"5_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/3-540-45319-9_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M.N. Velev","year":"2001","unstructured":"Velev, M.N.: Automatic abstraction of memories in the formal verification of superscalar microprocessors. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, p. 252. Springer, Heidelberg (2001)"},{"key":"5_CR66","doi-asserted-by":"crossref","unstructured":"Bryant, R.E., Lahiri, S., Seshia, S.: Modeling and Verifying Systems using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions. In: Proceedings of Conference on Computer Aided Verification (2002)","DOI":"10.1007\/3-540-45657-0_7"},{"key":"5_CR67","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/3-540-40922-X_23","volume-title":"Formal Methods in Computer-Aided Design","author":"P. Bjesse","year":"2000","unstructured":"Bjesse, P., Claessen, K.: SAT-based verification without state space traversal. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 372\u2013389. Springer, Heidelberg (2000)"},{"key":"5_CR68","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Proceedings of Conference on Computer Aided Verification, pp. 154\u2013169 (2000)","DOI":"10.1007\/10722167_15"},{"key":"5_CR69","doi-asserted-by":"crossref","unstructured":"Chauhan, P., Clarke, E.M., Kukula, J., Sapra, S., Veith, H., Wang, D.: Automated Abstraction Refinement for Model Checking Large State Spaces using SAT based Conflict Analysis. In: Proceedings of Conference on Formal Methods in CAD (FMCAD) (2002)","DOI":"10.1007\/3-540-36126-X_3"},{"key":"5_CR70","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Interpolation and SAT-based Model Checking. In: Proceedings of Conference on Computer-Aided Verification (2003)","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"5_CR71","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., E\u00e9n, 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":"5_CR72","doi-asserted-by":"crossref","unstructured":"Williams, P., Biere, A., Clarke, E.M., Gupta, A.: Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking. In: Proceedings of International Conference on Computer-Aided Verification, pp. 124\u2013138 (2000)","DOI":"10.1007\/10722167_13"},{"key":"5_CR73","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/3-540-45657-0_19","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2002","unstructured":"McMillan, K.L.: Applying SAT methods in unbounded symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 250. Springer, Heidelberg (2002)"},{"key":"5_CR74","doi-asserted-by":"crossref","unstructured":"Kang, H.-J., Park, I.-C.: SAT-based unbounded symbolic model checking. In: Proceedings of the Design Automation Conference (2003)","DOI":"10.1145\/776038.776043"},{"key":"5_CR75","doi-asserted-by":"crossref","unstructured":"Tang, D., Malik, S., Gupta, A., Ip, N.: Symmetry reduction in SAT-based model checking. In: Proceedings of the International Conference on Computer Aided Verification, pp. 125\u2013138 (2005)","DOI":"10.1007\/11513988_12"},{"key":"5_CR76","unstructured":"VIS Home page, http:\/\/www-cad.eecs.berkeley.edu\/~vis"},{"key":"5_CR77","volume-title":"The Industrial Information Technology Handbook","author":"A. Gupta","year":"2005","unstructured":"Gupta, A., Bayazit, A.A., Mahajan, Y.: Verification Languages. In: The Industrial Information Technology Handbook. CRC Press, Boca Raton (2005)"},{"key":"5_CR78","unstructured":"Williams, S.: Icarus Verilog, http:\/\/www.icarus.com\/eda\/verilog"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Hardware Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11757283_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,12]],"date-time":"2025-01-12T04:42:16Z","timestamp":1736656936000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11757283_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540343042","9783540343059"],"references-count":78,"URL":"https:\/\/doi.org\/10.1007\/11757283_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}