{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,16]],"date-time":"2026-06-16T10:36:24Z","timestamp":1781606184039,"version":"3.54.5"},"reference-count":109,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2005,1,25]],"date-time":"2005-01-25T00:00:00Z","timestamp":1106611200000},"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":[[2005,4]]},"DOI":"10.1007\/s10009-004-0183-4","type":"journal-article","created":{"date-parts":[[2005,1,24]],"date-time":"2005-01-24T15:01:13Z","timestamp":1106578873000},"page":"156-173","source":"Crossref","is-referenced-by-count":178,"title":["A survey of recent advances in SAT-based formal verification"],"prefix":"10.1007","volume":"7","author":[{"given":"Mukul R.","family":"Prasad","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Armin","family":"Biere","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2005,1,25]]},"reference":[{"key":"183_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla PA, Bjesse P, E\u00e9n N (2000) Symbolic reachability analysis based on SAT-solvers. In: Graf S, Schwartzbach M (eds) Proceedings of the 6th international conference on tools and algorithms for the construction and analysis of systems (TACAS), March 2000. Lecture notes in computer science, vol 1785. Springer, Berlin Heidelberg New York, pp 411\u2013425","DOI":"10.1007\/3-540-46419-0_28"},{"key":"183_CR2","doi-asserted-by":"crossref","unstructured":"Abraham JA, Vedula VM, Saab DG (2002) Verifying properties using sequential ATPG. In: Proceedings of the International Test Conference (ITC), October 2002, pp 194\u2013202","DOI":"10.1109\/TEST.2002.1041761"},{"key":"183_CR3","doi-asserted-by":"crossref","unstructured":"Alur R (1999) Timed automata. In: Halbwachs N, Peled D (eds) Proceedings of the 11th international conference on computer-aided verification (CAV), July 1999. Lecture notes in computer science, vol 1633. Springer, Berlin Heidelberg New York, pp 8\u201322","DOI":"10.1007\/3-540-48683-6_3"},{"key":"183_CR4","doi-asserted-by":"crossref","unstructured":"Amla N, Kurshan R, McMillan K, Medel R (2003) Experimental analysis of different techniques for bounded model checking. In: Garavel H, Hatcliff J (eds) Proceedings of the 9th international conference on tools and algorithms for the construction and analysis of systems (TACAS), April 2003. Lecture notes in computer science, vol 2619. Springer, Berlin Heidelberg New York, pp 34\u201348","DOI":"10.1007\/3-540-36577-X_4"},{"key":"183_CR5","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1006\/inco.2001.2948","volume":"179","author":"Andersen","year":"2002","unstructured":"Andersen HR, Hulgaard H (2002) Boolean expression diagrams. Inf Comput 179(2):194\u2013212","journal-title":"Inf Comput"},{"key":"183_CR6","doi-asserted-by":"crossref","unstructured":"Ayari A, Basin D (2000) Bounded model construction for monadic second-order logics. In: Emerson EA, Sistla AP (eds) Proceedings of the 12th international conference on computer-aided verification (CAV), July 2000. Lecture notes in computer science, vol 1855. Springer, Berlin Heidelberg New York, pp 99\u2013113","DOI":"10.1007\/10722167_11"},{"key":"183_CR7","doi-asserted-by":"crossref","unstructured":"Ayari A, Basin D (2002) QUBOS: Deciding quantified Boolean logic using propositional satisfiability solvers. In: Aagard M, O\u2019Leary JW (eds) Proceedings of the 4th international conference on formal methods in computer-aided design (FMCAD). Lecture notes in computer science, vol 2517. Springer, Berlin Heidelberg New York, pp 187\u2013201","DOI":"10.1007\/3-540-36126-X_12"},{"key":"183_CR8","doi-asserted-by":"crossref","unstructured":"Ball T, Rajamani SK (2002) The SLAM project: debugging system soft-ware via static analysis. In: Proceedings of the 29th SIGPLAN-SIGACT symposium on principles of programming languages (POPL) January 2002. ACM Press, New York, pp 1\u20133","DOI":"10.1145\/503272.503274"},{"key":"183_CR9","doi-asserted-by":"crossref","unstructured":"Barrett CW, Dill DL, Stump A (2002) Checking satisfiability of first-order formulas by incremental translation to SAT. In: Brinksma E, Larsen KG (eds) Proceedings of the 14th international conference on computer-aided verification (CAV), July 2002. Lecture notes in computer science, vol 2404. Springer, Berlin Heidelberg New York, pp 236\u2013249","DOI":"10.1007\/3-540-45657-0_18"},{"key":"183_CR10","doi-asserted-by":"crossref","unstructured":"Baumgartner J, Kuehlmann A, Abraham JA (2002) Property Checking via Structural Analysis. In: Brinksma E, Larsen KG (eds) Proceedings of the 14th international conference on computer-aided verification (CAV), July 2002. Lecture notes in computer science, vol 2404. Springer, Berlin Heidelberg New York, pp 151\u2013165","DOI":"10.1007\/3-540-45657-0_12"},{"key":"183_CR11","unstructured":"Bayardo RJ, Schrag RC (1997) Using CSP look-back techniques to solve real-world SAT instances. In: Proceedings of the national conference on artificial intelligence (AAAI), July 1997, pp 203\u2013208"},{"key":"183_CR12","doi-asserted-by":"crossref","unstructured":"Le Berre D, Simon L, Tachella A (2004) Challenges in the QBF arena: the SAT\u201903 evaluation of QBF solvers. In: Giunchiglia E, Tacchella A (eds) Proceedings of the 6th international conference on theory and applications of satisfiability testing (SAT), May 2004. Lecture notes in computer science, vol 2919. Springer, Berlin Heidelberg New York, pp 468\u2013485","DOI":"10.1007\/978-3-540-24605-3_35"},{"key":"183_CR13","unstructured":"Biere A (2004) Resolve and expand. In: Proceedings of the 7th international conference on theory and applications of satisfiability testing (SAT), May 2004"},{"key":"183_CR14","doi-asserted-by":"crossref","unstructured":"Biere A, Cimatti A, Clarke EM, Fujita M, Zhu Y (1999) Symbolic model checking using SAT procedures instead of BDDs. In: Proceedings of the 36th conference on design automation (DAC), June 1999, pp 317\u2013320","DOI":"10.1109\/DAC.1999.781333"},{"key":"183_CR15","doi-asserted-by":"crossref","unstructured":"Biere A, Cimatti A, Clarke EM, Zhu Y (1999) Symbolic model checking without BDDs. In: Cleaveland R (ed) Proceedings of the 5th international conference on tools and algorithms for the construction and analysis of systems (TACAS), March 1999. Lecture notes in computer science, vol 1579. Springer, Berlin Heidelberg New York, pp 193\u2013207","DOI":"10.1007\/3-540-49059-0_14"},{"key":"183_CR16","doi-asserted-by":"crossref","unstructured":"Biere A, Clarke E, Raimi R, Zhu Y (1999) Verifying safety properties of a PowerPC microprocessor using symbolic model checking without BDDs. In: Halbwachs N, Peled D (eds) Proceedings of the 11th international conference on computer-aided verification (CAV), July 1999. Lecture notes in computer science, vol 1633. Springer, Berlin Heidelberg New York, pp 60\u201371","DOI":"10.1007\/3-540-48683-6_8"},{"key":"183_CR17","doi-asserted-by":"crossref","unstructured":"Biere A, Clarke EM, Zhu Y (1999) Multiple state and single state tableaux for combining local and global model checking. In: Olderog E-R, Steffen B (eds) Correct system design, recent insight and advances. Lecture notes in computer science, vol 1710. Springer, Berlin Heidelberg New York, pp 163\u2013179","DOI":"10.1007\/3-540-48092-7_8"},{"key":"183_CR18","doi-asserted-by":"crossref","unstructured":"Bjesse P, Claessen K (2000) SAT-based verification without state space traversal. In: Hunt Jr WA, Johnson SD (eds) Proceedings of the 3rd international conference on formal methods in computer-aided design (FMCAD), November 2000. Lecture notes in computer science, vol 1954. Springer, Berlin Heidelberg New York, pp 372\u2013389","DOI":"10.1007\/3-540-40922-X_23"},{"key":"183_CR19","doi-asserted-by":"crossref","unstructured":"Bjesse P, Leonard T, Mokkedem A (2001) Finding bugs in an alpha microprocessor using satisfiability solvers. In: Berry G, Comon H, Finkel A (eds) Proceedings of the 13th international conference on computer-aided verification (CAV), July 2001. Lecture notes in computer science, vol 2102. Springer, Berlin Heidelberg New York, pp 454\u2013464","DOI":"10.1007\/3-540-44585-4_44"},{"key":"183_CR20","doi-asserted-by":"crossref","unstructured":"Boppana V, Rajan SP, Takayama K, Fujita M (1999) Model checking based on sequential ATPG. In: Halbwachs N, Peled D (eds) Proceedings of the 11th international conference on computer-aided verification (CAV), July 1999. Lecture notes in computer science, vol 1633. Springer, Berlin Heidelberg New York, pp 418\u2013430","DOI":"10.1007\/3-540-48683-6_36"},{"key":"183_CR21","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C","author":"Bryant","year":"1986","unstructured":"Bryant RE (1986) Graph based algorithms for Boolean function manipulation. IEEE Trans Comput C(35):677\u2013691","journal-title":"IEEE Trans Comput"},{"key":"183_CR22","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1109\/43.275352","volume":"13","author":"Burch","year":"1994","unstructured":"Burch JR, Clarke EM, Long DE, McMillan KL, Dill DL (1994) Symbolic model checking for sequential circuit verification. IEEE Trans Comput Aided Des Integ Circuits Syst 13(4):401\u2013424","journal-title":"IEEE Trans Comput Aided Des Integ Circuits Syst"},{"key":"183_CR23","doi-asserted-by":"crossref","unstructured":"Cabodi G, Nocco S, Quer S (2003) Improving SAT-based bounded model checking by means of BDD-based approximate traversals. In: Proceedings of Design Automation and Test in Europe (DATE), March 2003, pp 898\u2013903","DOI":"10.1109\/DATE.2003.1253720"},{"key":"183_CR24","unstructured":"Cadoli M, Giovanardi A, Schaerf M (1998) An algorithm to evaluate quantified Boolean formulae. In: Proceedings of the 15th national conference on artificial intelligence (AAAI), July 1998, pp 262\u2013267"},{"key":"183_CR25","doi-asserted-by":"crossref","unstructured":"Chauhan P, Clarke EM, Kukula J, Sapra S, Veith H, Wang D (2002) Automated abstraction refinement for model checking large state spaces using SAT based conflict analysis. In: Aagaard M, O\u2019Leary JW (eds) Proceedings of the 4th international conference on formal methods in computer-aided design (FMCAD), November 2002. Lecture notes in computer science, vol 2517. Springer, Berlin Heidelberg New York, pp 33\u201351","DOI":"10.1007\/3-540-36126-X_3"},{"key":"183_CR26","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"Clarke","year":"2001","unstructured":"Clarke E, Biere A, Raimi R, Zhu Y (2001) Bounded model checking using satisfiability solving. Formal Methods Syst Des 19(1):7\u201334","journal-title":"Formal Methods Syst Des"},{"key":"183_CR27","doi-asserted-by":"crossref","unstructured":"Clarke EM, Emerson EA (1982) Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen D (ed) Proceedings of the workshop on logic of programs. Lecture notes in computer science, vol 131. Springer, Berlin Heidelberg New York, pp 52\u201371","DOI":"10.1007\/BFb0025774"},{"key":"183_CR28","unstructured":"Clarke EM, Grumberg O, Peled DA (2000) Model checking. MIT Press, Cambridge, MA"},{"key":"183_CR29","doi-asserted-by":"crossref","unstructured":"Clarke EM, Gupta A, Kukula J, Strichman O (2002) SAT-based abstraction refinement using ILP and machine learning techniques. In: Brinksma E, Larsen KG (eds) Proceedings of the 14th international conference on computer-aided verification (CAV), July 2002. Lecture notes in computer science, vol 2404. Springer, Berlin Heidelberg New York, pp 265\u2013279","DOI":"10.1007\/3-540-45657-0_20"},{"key":"183_CR30","doi-asserted-by":"crossref","unstructured":"Clarke EM, Schlingloff B-H (2001) Model checking. In: Robinson JA, Voronkov A (eds) Handbook of automated reasoning, vol 2. Elsevier\/MIT Press, Amsterdam\/Cambridge, MA, pp 1635\u20131790","DOI":"10.1016\/B978-044450813-3\/50026-6"},{"key":"183_CR31","doi-asserted-by":"crossref","unstructured":"Copti F, Fix L, Fraer R, Giunchiglia E, Kamhi G, Tacchella A, Vardi MY (2001) Benefits of bounded model checking in an industrial setting. In: Berry G, Comon H, Finkel A (eds) Proceedings of the 13th international conference on computer-aided verification (CAV), July 2001. Lecture notes in computer science, vol 2102. Springer, Berlin Heidelberg New York, pp 436\u2013453","DOI":"10.1007\/3-540-44585-4_43"},{"key":"183_CR32","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"Davis","year":"1962","unstructured":"Davis M, Logemann G, Loveland D (1962) A machine program for theorem-proving. Commun ACM 5(7):394\u2013397","journal-title":"Commun ACM"},{"key":"183_CR33","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"Davis","year":"1960","unstructured":"Davis M, Putnam H (1960) A computing procedure for quantification theory. J ACM 7(3):201\u2013215","journal-title":"J ACM"},{"key":"183_CR34","unstructured":"Donini FM, Liberatore P, Massacci F, Schaerf M (2002) Solving QBF with SMV. In: Proceedings of the 8th international conference on principles of knowledge representation and reasoning (KR), pp 578\u2013589"},{"key":"183_CR35","doi-asserted-by":"crossref","unstructured":"E\u00e9n N, S\u00f6rensson N (2003) Temporal induction by incremental SAT solving. In: Strichman O, Biere A (eds) Proceedings of the 1st international workshop on bounded model checking (BMC), July 2003. Electronic notes in theoretical computer science, vol 89. Elsevier, Amsterdam","DOI":"10.1016\/S1571-0661(05)82542-3"},{"key":"183_CR36","doi-asserted-by":"crossref","unstructured":"Emerson EA (1990) Temporal and modal logic, vol B. MIT Press, Cambridge, MA, pp 995\u20131072","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"183_CR37","doi-asserted-by":"crossref","unstructured":"Fallah F (2002) Binary time-frame expansion. In: Proceedings of the international conference on computer-aided design (ICCAD), November 2002, pp 458\u2013464","DOI":"10.1145\/774572.774639"},{"key":"183_CR38","doi-asserted-by":"crossref","unstructured":"Fujiwara H, Shimono T (1983) On the acceleration of test generation algorithms. IEEE Trans Comput C-32:1137\u20131144","DOI":"10.1109\/TC.1983.1676174"},{"key":"183_CR39","doi-asserted-by":"crossref","unstructured":"Ganai MK, Aziz A (2002) Improved SAT-based bounded reachability analysis. In: Proceedings of the 15th international conference on VLSI design (VLSID), January 2002, pp 729\u2013734","DOI":"10.1109\/ASPDAC.2002.995020"},{"key":"183_CR40","doi-asserted-by":"crossref","unstructured":"Ganai MK, Gupta A, Ashar P (2004) Efficient SAT-based unbounded symbolic model checking using circuit cofactoring. In: Proceedings of the international conference on computer-aided design (ICCAD), November 2004","DOI":"10.1109\/ICCAD.2004.1382631"},{"key":"183_CR41","doi-asserted-by":"crossref","unstructured":"Ganai MK, Zhang L, Ashar P, Gupta A (2002) Combining strengths of circuit-based and CNF-based algorithms for a high performance SAT solver. In: Proceedings of the 39th conference on design automation (DAC), June 2002, pp 747\u2013750","DOI":"10.1109\/DAC.2002.1012722"},{"key":"183_CR42","first-page":"a","volume":"intractability","author":"Garey","year":"1979","unstructured":"Garey MR, Johnson DS (1979) Computers and intractability: a guide to the theory of NP-completeness. Freeman, San Francisco","journal-title":"Computers and"},{"key":"183_CR43","unstructured":"Giunchiglia E, Narizzano M, Tacchella A (2002) Learning for quantified Boolean logic satisfiability. In: Proceedings of the 18th national conference on artificial intelligence (AAAI), July 2002, pp 649\u2013654"},{"key":"183_CR44","doi-asserted-by":"crossref","unstructured":"Goel P (1981) An implicit enumeration algorithm to generate tests for combinational logic circuits. IEEE Trans Comput C-30:215\u2013222","DOI":"10.1109\/TC.1981.1675757"},{"key":"183_CR45","doi-asserted-by":"crossref","unstructured":"Goldberg E, Novikov Y (2002) BerkMin: a fast and robust SAT-solver. In: Proceedings of Design Automation and Test in Europe (DATE), March 2002, pp 142\u2013149","DOI":"10.1109\/DATE.2002.998262"},{"key":"183_CR46","doi-asserted-by":"crossref","unstructured":"Goldberg E, Novikov Y (2003) Verification of proofs of unsatisfiability for CNF formulas. In: Proceedings of Design Automation and Test in Europe (DATE), March 2003, pp 886\u2013891","DOI":"10.1109\/DATE.2003.1253718"},{"key":"183_CR47","doi-asserted-by":"crossref","unstructured":"Goldberg E, Prasad MR, Brayton RK (2001) Using SAT for combinational equivalence checking. In: Proceedings of Design Automation and Test in Europe (DATE), March 2001, pp 114\u2013121","DOI":"10.1109\/DATE.2001.915010"},{"key":"183_CR48","doi-asserted-by":"crossref","unstructured":"Gupta A, Ganai M, Wang C, Yang Z, Ashar P (2003) Abstraction and BDDs complement SAT-based BMC in DiVer. In: Hunt Jr WA, Somenzi F (eds) Proceedings of the 15th international conference on computer-aided verification (CAV), July 2003. Lecture notes in computer science, vol 2725. Springer, Berlin Heidelberg New York, pp 206\u2013209","DOI":"10.1007\/978-3-540-45069-6_20"},{"key":"183_CR49","doi-asserted-by":"crossref","unstructured":"Gupta A, Ganai M, Wang C, Yang Z, Ashar P (2003) Learning from BDDs in SAT-based bounded model checking. In: Proceedings of the 40th conference on design automation (DAC), June 2003, pp 824\u2013829","DOI":"10.1109\/DAC.2003.1219133"},{"key":"183_CR50","doi-asserted-by":"crossref","unstructured":"Gupta A, Ganai M, Yang Z, Ashar P (2003) Iterative abstraction using SAT-based BMC with proof analysis. In: Proceedings of the international conference on computer-aided design (ICCAD), November 2003, pp 416\u2013423","DOI":"10.1109\/ICCAD.2003.1257811"},{"key":"183_CR51","doi-asserted-by":"crossref","unstructured":"Gupta A, Gupta A, Yang Z, Ashar P (2001) Dynamic detection and removal of inactive clauses in SAT with application in image computation. In: Proceedings of the 38th conference on design automation, June 2001, pp 536\u2013541","DOI":"10.1145\/378239.379018"},{"key":"183_CR52","unstructured":"Gupta A, Yang Z, Ashar P, Gupta A (2000) SAT based state reachability analysis and model checking. In: Hunt WA, Johnson SD (eds) Proceedings of the 3rd international conference on formal methods in computer-aided design (FMCAD), November 2000. Lecture notes in computer science, vol 1954. Springer, Berlin Heidelberg New York, pp 354\u2013371"},{"key":"183_CR53","doi-asserted-by":"crossref","unstructured":"Gupta A, Yang Z, Ashar P, Zhang L, Malik S (2001) Partition-based decision heuristics for image computation using SAT and BDDs. In: Proceedings of the international conference on computer-aided design (ICCAD), November 2001, pp 286\u2013292","DOI":"10.1109\/ICCAD.2001.968635"},{"key":"183_CR54","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Kupferman O, Qadeer S (1998) From pre-historic to post-modern symbolic model checking. In: Hu AJ, Vardi MY (eds) Proceedings of the 10th international conference on computer-aided verification (CAV), July 1998. Lecture notes in computer science, vol 1427. Springer, Berlin Heidelberg New York, pp 195\u2013206","DOI":"10.1007\/BFb0028745"},{"key":"183_CR55","unstructured":"Holzmann GJ (1991) Design and validation of computer protocols. Prentice Hall, Upper Saddle River, NJ"},{"key":"183_CR56","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1109\/43.913756","volume":"20","author":"Huan","year":"2001","unstructured":"Huan C-Y, Cheng K-T (2001) Using word-level ATPG and modular arithmetic constraint-solving techniques for assertion property checking. IEEE Trans Comput Aided Des 20(3):381\u2013391","journal-title":"IEEE Trans Comput Aided Des"},{"key":"183_CR57","doi-asserted-by":"crossref","unstructured":"Iwashita H, Nakata T (1997) Forward model checking techniques oriented to buggy designs. In: Proceedings of the international conference on computer-aided design (ICCAD), November 1997, pp 400\u2013404","DOI":"10.1109\/ICCAD.1997.643567"},{"key":"183_CR58","doi-asserted-by":"crossref","unstructured":"Iwashita H, Nakata T, Hirose F (1996) CTL model checking based on forward state traversal. In: Proceedings of the international conference on computer-aided design (ICCAD), November 1996, pp 82\u201387","DOI":"10.1109\/ICCAD.1996.569084"},{"key":"183_CR59","doi-asserted-by":"crossref","unstructured":"Iyer MK, Parthasarathy G, Cheng K-T (2003) SATORI \u2013 A fast sequential SAT engine for circuits. In: Proceedings of the international conference on computer-aided design (ICCAD), November 2003, pp 320\u2013325","DOI":"10.1109\/ICCAD.2003.159706"},{"key":"183_CR60","doi-asserted-by":"crossref","unstructured":"Jackson D, Vaziri M (2000) Finding bugs with a constraint solver. In: Proceedings of the international symposium on software testing and analysis (ISSTA), August 2000, pp 14\u201325","DOI":"10.1145\/347324.383378"},{"key":"183_CR61","unstructured":"Kim J, Whittemore J, Sakallah K (2000) On solving stack-based incremental satisfiability problems. In: Proceedings of the international conference on computer design (ICCD), October 2000, pp 379\u2013382"},{"key":"183_CR62","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"Kleine","year":"1995","unstructured":"Kleine B\u00fcning H, Karpinski M, Fl\u00f6gel A (1995) Resolution for quantified boolean formulas. Inf Comput 117(1):12\u201318","journal-title":"Inf Comput"},{"key":"183_CR63","first-page":"deduction","volume":"logic","author":"Kleine","year":"1999","unstructured":"Kleine B\u00fcning H, Lettmann T (1999) Propositional logic: deduction and algorithms, Cambridge tracts in theoretical computer science, vol 48. Cambridge University Press, Cambridge, UK. ISBN-0-521-63017-7","journal-title":"Propositional"},{"key":"183_CR64","doi-asserted-by":"crossref","first-page":"1377","DOI":"10.1109\/TCAD.2002.804386","volume":"21","author":"Kuehlmann","year":"2002","unstructured":"Kuehlmann A, Paruthi V, Krohm F, Ganai MK (2002) Robust Boolean reasoning for equivalence checking and functional property verification. IEEE Trans Comput Aided Des Integ Circuits Syst 21(12):1377\u20131394","journal-title":"IEEE Trans Comput Aided Des Integ Circuits Syst"},{"key":"183_CR65","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1109\/43.108614","volume":"11","author":"Larrabee","year":"1992","unstructured":"Larrabee T (1992) Test pattern generation using Boolean satisfiability. IEEE Trans Comput Aided Des Integ Circuits Syst 11(1):4\u201315","journal-title":"IEEE Trans Comput Aided Des Integ Circuits Syst"},{"key":"183_CR66","doi-asserted-by":"crossref","unstructured":"Letz R (2002) Lemma and model caching in decision procedures for quantified Boolean formulas. In: Egly U, Ferm\u00fcller CG (eds) Proceedings of the international conference on automated reasoning with analytic tableaux and related methods (TABLEAUX), July 2002. Lecture notes in computer science, vol 2381. Springer, Berlin Heidelberg New York","DOI":"10.1007\/3-540-45616-3_12"},{"key":"183_CR67","doi-asserted-by":"crossref","unstructured":"Li B, Wang C, Somenzi F (2003) A satisfiability-based approach to abstraction refinement in model checking. In: Proceedings of the 1st international workshop on bounded model checking (BMC), July 2003. Electronic notes in theoretical computer science, vol 89. Elsevier, Amsterdam","DOI":"10.1016\/S1571-0661(05)82546-0"},{"key":"183_CR68","doi-asserted-by":"crossref","unstructured":"Lu F, Wang L-C, Cheng K-T, Moondanos J, Hanna Z (2003) A signal correlation guided ATPG solver and its applications for solving difficult industrial cases. In: Proceedings of the 40th conference on design automation (DAC), June 2003, pp 436\u2013441","DOI":"10.1145\/775832.775947"},{"key":"183_CR69","unstructured":"Lu F, Wang L-C, Cheng K-T, Huang RC-Y (2003) A circuit SAT solver with signal correlation guided learning. In: Proceedings of Design Automation and Test in Europe (DATE), March 2003, pp 892\u2013897"},{"key":"183_CR70","doi-asserted-by":"crossref","unstructured":"Marques-Silva JP (1999) The impact of branching heuristics in propositional satisfiability algorithms. In: Proceedings of the 9th Portuguese conference on artificial intelligence (EPIA), September 1999","DOI":"10.1007\/3-540-48159-1_5"},{"key":"183_CR71","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/12.769433","volume":"48","author":"Marques-Silva","year":"1999","unstructured":"Marques-Silva JP, Sakallah KA (1999) GRASP: A search algorithm for propositional satisfiability. IEEE Trans Comput 48(5):506\u2013521","journal-title":"IEEE Trans Comput"},{"key":"183_CR72","first-page":"an","volume":"checking","author":"McMillan","year":"1993","unstructured":"McMillan KL (1993) Symbolic model checking: an approach to the state explosion problem. Kluwer, Dordrecht","journal-title":"Symbolic model"},{"key":"183_CR73","doi-asserted-by":"crossref","unstructured":"McMillan KL (2002) Applying SAT methods in unbounded symbolic model checking. In: Brinksma E, Larsen KG (eds) Proceedings of the 14th international conference on computer-aided verification, July 2002. Lecture notes in computer science, vol 2404. Springer, Berlin Heidelberg New York, pp 250\u2013264","DOI":"10.1007\/3-540-45657-0_19"},{"key":"183_CR74","doi-asserted-by":"crossref","unstructured":"McMillan KL (2003) Interpolation and SAT-based model checking. In: Hunt Jr WA, Somenzi F (eds) Proceedings of the 15th conference on computer-aided verification (CAV), July 2003. Lecture notes in computer science, vol 2725. Springer, Berlin Heidelberg New York, pp 1\u201313","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"183_CR75","doi-asserted-by":"crossref","unstructured":"McMillan KL, Amla N (2003) Automatic abstraction without counterexamples. In: Garavel H, Hatcliff J (eds) Proceedings of the international conference on tools and algorithms for the construction and analysis of systems (TACAS), April 2003. Lecture notes in computer science, vol 2619. Springer, Berlin Heidelberg New York, pp 2\u201317","DOI":"10.1007\/3-540-36577-X_2"},{"key":"183_CR76","unstructured":"Mneimneh M, Sakallah K (2002) SAT-based sequential depth computation. In: Proceedings of the 1st international workshop on constraints in formal verification, September 2002"},{"key":"183_CR77","doi-asserted-by":"crossref","unstructured":"Moskewicz MH, Madigan CF, Zhao Y, Zhang L, Malik S (2001) Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th conference on design automation (DAC), June 2001, pp 530\u2013535","DOI":"10.1145\/378239.379017"},{"key":"183_CR78","doi-asserted-by":"crossref","unstructured":"Parthasarthy G, Huang C-Y, Cheng K-T (2001) An analysis of ATPG and SAT algorithms for formal verification. In: Proceedings of the 6th international workshop on high-level design validation and test (HLDVT), November 2001, pp 177\u2013182","DOI":"10.1109\/HLDVT.2001.972826"},{"key":"183_CR79","doi-asserted-by":"crossref","unstructured":"Kurshan RP (1995) Computer-aided verification of coordinating processes: the automata-theoretic approach. Princeton University Press, Princeton, NJ","DOI":"10.1515\/9781400864041"},{"key":"183_CR80","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/S0166-218X(02)00409-2","volume":"130","author":"Plaisted","year":"2003","unstructured":"Plaisted D, Biere A, Zhu Y (2003) A satisfiability procedure for quantified Boolean formulae. Discrete Appl Math 130(2):291\u2013328","journal-title":"Discrete Appl Math"},{"key":"183_CR81","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"Plaisted","year":"1986","unstructured":"Plaisted D, Greenbaum S (1986) A structure-preserving clause form translation. J Symbol Comput 2(3):293\u2013304","journal-title":"J Symbol Comput"},{"key":"183_CR82","doi-asserted-by":"crossref","unstructured":"Rintanen J (2001) Partial implicit unfolding in the Davis-Putnam procedure for quantified boolean formulae. In: International conference on logic for programming, artificial intelligence and reasoning (LPAR)","DOI":"10.1007\/3-540-45653-8_25"},{"key":"183_CR83","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/S0022-0000(70)80006-X","volume":"4","author":"Savitch","year":"1970","unstructured":"Savitch WJ (1970) Relational between nondeterministic and deterministic tape complexity. J Comput Syst Sci 4:177\u2013192","journal-title":"J Comput Syst Sci"},{"key":"183_CR84","doi-asserted-by":"crossref","unstructured":"Schuppan V, Biere A (2004) Efficient reduction of finite state model checking to reachability analysis. Int J Softw Tools Technol Transfer 5(1\u20132):185\u2013204","DOI":"10.1007\/s10009-003-0121-x"},{"key":"183_CR85","unstructured":"Selman B, Kautz HA, Cohen B (1994) Noise strategies for improving local search. In: Proceedings of the 12th national conference on artificial intelligence (AAAI), July 1994, pp 337\u2013343"},{"key":"183_CR86","unstructured":"Selman B, Levesque HJ, Mitchell D (1992) A new method for solving hard satisfiability problems. In: Proceedings of the 10th national conference on artificial intelligence (AAAI), July 1992, pp 440\u2013446"},{"key":"183_CR87","doi-asserted-by":"crossref","unstructured":"Seshia SA, Lahiri SK, Bryant RE (2003) A hybrid SAT-based decision procedure for separation logic with uninterpreted functions. In: Proceedings of the 40th conference on design automation (DAC), June 2003, pp 425\u2013430","DOI":"10.1109\/DAC.2003.1219039"},{"key":"183_CR88","doi-asserted-by":"crossref","unstructured":"Shacham O, Zarpas E (2003) Tuning the VSIDS decision heuristic for bounded model checking. In: Proceedings of the 4th international workshop on microprocessor test and verification (MTV), May 2003, pp 75\u201379","DOI":"10.1109\/MTV.2003.1250266"},{"key":"183_CR89","doi-asserted-by":"crossref","unstructured":"Sheeran M, Singh S, St\u00e5lmarck G (2000) Checking safety properties using induction, a SAT-solver. In: Hunt Jr WA, Johnson SD (eds) Proceedings of the 3rd international conference on formal methods in computer-aided design (FMCAD), November 2000. Lecture notes in computer science, vol 1954. Springer, Berlin Heidelberg New York, pp 108\u2013125","DOI":"10.1007\/3-540-40922-X_8"},{"key":"183_CR90","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1023\/A:1008725524946","volume":"16","author":"Sheeran","year":"2000","unstructured":"Sheeran M, St\u00e5lmarck G (2000) A tutorial on St\u00e5lmarck\u2019s proof procedure for propositional logic. Formal Methods Syst Des 16(1):23\u201358","journal-title":"Formal Methods Syst Des"},{"key":"183_CR91","unstructured":"Sheng S, Takayama K, Hsiao MS (2002) Effective static property checking using simulation-based ATPG. In: Proceedings of the 39th conference on design automation (DAC), June 2002, pp 813\u2013818"},{"key":"183_CR92","unstructured":"Shtrichman O (2000) Sharing information between instances of propositional satisfiability (SAT) problems, January 2000. US patent (Disclosure no.: IL8-2000-0070)"},{"key":"183_CR93","unstructured":"Stockmeyer LJ, Meyer AR (1973) Word problems requiring exponential time. In: Proceedings of the 5th annual ACM symposium on the theory of computing (STOC), pp 1\u20139"},{"key":"183_CR94","doi-asserted-by":"crossref","unstructured":"Stoffel D, Kunz W (1997) Record and play: a structural fixed point iteration for sequential circuit verification. In: Proceedings of the international conference on computer-aided design (ICCAD), November 1997, pp 394\u2013399","DOI":"10.1109\/ICCAD.1997.643566"},{"key":"183_CR95","unstructured":"Strichman O (2000) Tuning SAT checkers for bounded model checking. In: Emerson EA, Sistla AP (eds) Proceedings of the 12th international conference on computer-aided verification (CAV), July 2000. Lecture notes in computer science, vol 1855. Springer, Berlin Heidelberg New York, pp 480\u2013494"},{"key":"183_CR96","unstructured":"Strichman O (2001) Pruning techniques for the SAT-based bounded model checking problem. In: Margaria T, Melham TF (eds) Proceedings of the 11th advanced research working conference on correct hardware design and verification methods (CHARME), September 2001. Lecture notes in computer science, vol 2144. Springer, Berlin Heidelberg New York, pp 58\u201370"},{"key":"183_CR97","doi-asserted-by":"crossref","unstructured":"Strichman O (2002) On solving Presburger and linear arithmetic with SAT. In: Aagaard M, O\u2019Leary JW (eds) Proceedings of the 4th international conference on formal methods in computer-aided design (FMCAD), November 2002. Lecture notes in computer science, vol 2517. Springer, Berlin Heidelberg New York, pp 160\u2013170","DOI":"10.1007\/3-540-36126-X_10"},{"key":"183_CR98","unstructured":"Tseitin GS (1968) On the complexity of derivation in propositional calculus. In: Slisenko AO (ed) Studies in constructive mathematics and mathematical logic. Seminars in mathematics, vol 8. Steklov Mathematical Institute, Leningrad, Russia, pp 234\u2013259 (English Translation: Consultants Bureau, New York, 1970, pp 115\u2013125)"},{"key":"183_CR99","doi-asserted-by":"crossref","unstructured":"van Eijk CAJ (1998) Sequential equivalence checking without state space traversal. In: Proceedings of Design Automation and Test in Europe (DATE), February 1998, pp 618\u2013623","DOI":"10.1109\/DATE.1998.655922"},{"key":"183_CR100","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/S0747-7171(02)00091-3","volume":"35","author":"Velev","year":"2003","unstructured":"Velev MN, Bryant RE (2003) Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. J Symbol Comput 35(2):73\u2013106","journal-title":"J Symbol Comput"},{"key":"183_CR101","unstructured":"Wang C, Li B, Jin HS, Hachtel GD, Somenzi F (2003) Improving Ariadne\u2019s bundle by following multiple threads in abstraction refinement. In: Proceedings of the international conference on computer-aided design (ICCAD), November 2003, pp 408\u2013415"},{"key":"183_CR102","doi-asserted-by":"crossref","unstructured":"Whittemore JP, Kim J, Sakallah KA (2001) SATIRE: A new incremental satisfiability engine. In: Proceedings of the 38th conference on design automation (DAC), June 2001, pp 542\u2013545","DOI":"10.1145\/378239.379019"},{"key":"183_CR103","doi-asserted-by":"crossref","unstructured":"Williams PF, Biere A, Clarke EM, Gupta A (2000) Combining decision diagrams and SAT procedures for efficient symbolic model checking. In: Emerson EA, Sistla AP (eds) Proceedings of the 12th international conference on computer-aided verification (CAV), July 2000. Lecture notes in computer science, vol 1855. Springer, Berlin Heidelberg New York, pp 124\u2013138","DOI":"10.1007\/10722167_13"},{"key":"183_CR104","unstructured":"Yen C-C, Chen K-C, Jou J-Y (2002) A practical approach to cycle bound estimation for property checking. In: Proceedings of 11th international workshop on logic and synthesis (IWLS), June 2002, pp 149\u2013154"},{"key":"183_CR105","doi-asserted-by":"crossref","unstructured":"Zhang H (1997) SATO: An efficient propositional prover. In: McCune W (ed) Proceedings of the 14th international conference on automated deduction (CADE), July 1997. Lecture notes in computer science, vol 1249. Springer, Berlin Heidelberg New York, pp 272\u2013275","DOI":"10.1007\/3-540-63104-6_28"},{"key":"183_CR106","unstructured":"Zhang L, Madigan CF, Moskewicz MH, Malik S (2001) Efficient conflict driven learning in a Boolean satisfiability solver. In: Proceedings of the international conference on computer-aided design (ICCAD), November 2001, pp 279\u2013285"},{"key":"183_CR107","unstructured":"Zhang L, Malik S (2002) The quest for efficient Boolean satisfiability solvers. In: Brinksma E, Larsen KG (eds) Proceedings of the 14th international conference on computer-aided verification (CAV), July 2001. Lecture notes in computer science, vol 2404. Springer, Berlin Heidelberg New York, pp 17\u201336"},{"key":"183_CR108","unstructured":"Zhang L, Malik S (2002) Towards symmetric treatment of conflicts and satisfaction in quantified Boolean satisfiability solvers. In: Van Hentenryck P (ed) Proceedings of the 8th international conference on principles and practice of constraint programming (CP). Lecture notes in computer science, vol 2470. Springer, Berlin Heidelberg New York, pp 200\u2013215"},{"key":"183_CR109","unstructured":"Zhang L, Malik S (2003) Validating SAT solvers using an independent resolution-based checker: practical implementations and other applications. In: Proceedings of Design Automation and Test in Europe (DATE), March 2003, pp 880\u2013885"}],"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-004-0183-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-004-0183-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-004-0183-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,1]],"date-time":"2023-05-01T19:32:18Z","timestamp":1682969538000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-004-0183-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,1,25]]},"references-count":109,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2005,4]]}},"alternative-id":["183"],"URL":"https:\/\/doi.org\/10.1007\/s10009-004-0183-4","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,1,25]]}}}