{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,12,31]],"date-time":"2024-12-31T05:21:50Z","timestamp":1735622510984,"version":"3.32.0"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2005,1,1]],"date-time":"2005-01-01T00:00:00Z","timestamp":1104537600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Comput Sci Technol"],"published-print":{"date-parts":[[2005,1]]},"DOI":"10.1007\/s11390-005-0004-6","type":"journal-article","created":{"date-parts":[[2005,4,5]],"date-time":"2005-04-05T13:18:13Z","timestamp":1112707093000},"page":"38-47","source":"Crossref","is-referenced-by-count":7,"title":["Formal Verification Techniques Based on Boolean Satisfiability Problem"],"prefix":"10.1007","volume":"20","author":[{"given":"Xiao-Wei","family":"Li","sequence":"first","affiliation":[]},{"given":"Guang-Hui","family":"Li","sequence":"additional","affiliation":[]},{"given":"Ming","family":"Shao","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","unstructured":"Anastasakis D, Damiano R, Ma Hi-Keung T, Stanion T. A practical and efficient method for compare-point matching. In Proc. 39th ACM\/IEEE Design Automation Conference, New Orleans, 2002, pp. 305?310.","DOI":"10.1145\/513918.513997"},{"issue":"1?2","key":"CR2","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1023\/A:1008349024680","volume":"16","author":"J Park","year":"2000","unstructured":"Park J, Pixley C, Burns M, Cho H. An efficient logic equivalence checker for industrial circuits. Journal of Electronic Testing: Theory and Applications, 2000, 16(1?2): 91?106.","journal-title":"Journal of Electronic Testing: Theory and Applications"},{"key":"CR3","doi-asserted-by":"crossref","unstructured":"Burch J R, Singhal V. Robust latch mapping for combinational equivalence checking. In Proc. International Conference on Computer Aided Design, San Jose, 1998, pp. 563?569.","DOI":"10.1145\/288548.289087"},{"key":"CR4","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-5693-0","volume-title":"Formal Equivalence Checking and Design Debugging","author":"Huang Shi-Yu","year":"1998","unstructured":"Shi-Yu Huang, Kwang-Ting Cheng. Formal Equivalence Checking and Design Debugging. Boston: Kluwer Academic Publishers, 1998."},{"key":"CR5","doi-asserted-by":"crossref","unstructured":"Berman C L, Trevillyan L H. Functional comparison of logic designs for VLSI chips. In Proc. IEEE\/ACM Int. Conf. Computer-Aided Design, San Jose, California, 1989, pp. 456?459.","DOI":"10.1109\/ICCAD.1989.76990"},{"key":"CR6","doi-asserted-by":"crossref","unstructured":"Matsunaga Y. An efficient equivalence checker for combinational circuits. In Proc. 33th ACM\/IEEE Design Automation Conference, Las Vegas, 1996, pp. 629?634.","DOI":"10.1145\/240518.240637"},{"issue":"1","key":"CR7","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1023\/A:1016096020556","volume":"21","author":"R Mukherjee","year":"2002","unstructured":"Mukherjee R et al. Efficient combinational verification using overlapping local BDDs and a hash table. Formal Methods in System Design, 2002, 21(1): 95?101.","journal-title":"Formal Methods in System Design"},{"issue":"12","key":"CR8","doi-asserted-by":"crossref","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 K. Robust Boolean reasoning for equivalence checking and funtional property verification. IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, 2002, 21(12): 1377?1394.","journal-title":"IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems"},{"key":"CR9","doi-asserted-by":"crossref","unstructured":"Burch J R, Singhal V. Tight integration of combinational verification methods. In Proc. IEEE\/ACM International Conference on Computer-Aided Design, San Jose, 1998, pp. 570?576.","DOI":"10.1145\/288548.289088"},{"key":"CR10","doi-asserted-by":"crossref","unstructured":"Paruthi V, Kuehlmann A. Equivalence checking combining a structural SAT-solver, BDDs, and simulation. In Proc. IEEE\/ACM International Conference on Computer-Aided Design, San Jose, California, 2000, pp. 459?464.","DOI":"10.1109\/ICCD.2000.878323"},{"key":"CR11","doi-asserted-by":"crossref","unstructured":"Daniel Brand. Verification of large synthesized designs. In Proc. IEEE\/ACM International Conference on Computer-Aided Design, San Jose, California, 1993, pp. 534?537.","DOI":"10.1109\/ICCAD.1993.580110"},{"key":"CR12","doi-asserted-by":"crossref","unstructured":"Marques-Silva J, Glass T. Combinational equivalence checking using satisfiability and recursive learning. In Proc. IEEE\/ACM Design, Automation and Test in Europe, 1999, pp. 145?149.","DOI":"10.1145\/307418.307477"},{"key":"CR13","doi-asserted-by":"crossref","unstructured":"Goldberg E I, Prasad M R, Brayton R K. Using SAT for combinational equivalence checking. In Proc. IEEE\/ACM Design, Automation and Test in Europe, 2001, pp. 114?121.","DOI":"10.1109\/DATE.2001.915010"},{"key":"CR14","doi-asserted-by":"crossref","unstructured":"J Marques-Silva, Karem A Sakallah. GRASP ? A search algorithm for propositional satisfiability. IEEE Trans. Computers, May 1999, 48(5): 506?521.","DOI":"10.1109\/12.769433"},{"key":"CR15","doi-asserted-by":"crossref","unstructured":"Moskewicz M W, Madigan C F, Zhao Y, Zhang L, Malik S. Zchaff: Engineering an efficient SAT solver. In Proc. 38th ACM\/IEEE Design Automation Conference, Las Vegas, 2001, pp. 530?535.","DOI":"10.1145\/378239.379017"},{"key":"CR16","doi-asserted-by":"crossref","unstructured":"Goldberg E, Novikov Y. BerkMin: A fast and robust SAT-solver. In Proc. the IEEE\/ACM Design Automation, and Test in Europe (DATE), 2002, pp. 142?149.","DOI":"10.1109\/DATE.2002.998262"},{"issue":"1","key":"CR17","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"M Clarke Edmund","year":"2001","unstructured":"Edmund M Clarke, Armin Biere, Richard Raimi, Yunshan Zhu. Bounded model checking using satisfiability solving. Formal Methods in System Design, 2001, 19(1): 7?34.","journal-title":"Formal Methods in System Design"},{"key":"CR18","doi-asserted-by":"crossref","unstructured":"Pankaj Chauhan et al. Automated abstraction refinement for model checking large state spaces using SAT based conflict analysis. In Proc. Formal Methods in Computer-Aided Design, 4th International Conference, Portland, OR, USA, November 6?8, 2002. pp. 33?51.","DOI":"10.1007\/3-540-36126-X_3"},{"key":"CR19","unstructured":"Edmund M Clarke, Orna Grumberg, Doron Peled. Model Checking. MIT Press, 1999."},{"key":"CR20","unstructured":"Dong Wang. SAT-based abstraction refinement for hardware verification [Thesis]. May 2003. Carnegie Mellon University."},{"issue":"1?3","key":"CR21","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1016\/S0166-218X(00)00245-6","volume":"107","author":"K B\u00fcning Hans","year":"2000","unstructured":"Hans K B\u00fcning. On subclasses of minimal unsatisfiable formulas. Discrete Applied Mathematics, 2000, 107(1?3): 83?98.","journal-title":"Discrete Applied Mathematics"},{"issue":"1","key":"CR22","doi-asserted-by":"crossref","first-page":"503","DOI":"10.1016\/S0304-3975(01)00337-1","volume":"289","author":"Fleischner Herbert","year":"2002","unstructured":"Herbert Fleischner et al. Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference. Theoretical Computer Science, 2002, 289(1): 503?516.","journal-title":"Theoretical Computer Science"},{"key":"CR23","unstructured":"Lintao Zhang, Sharad Malik. Extracting small unsatisfiable cores from unsatisfiable Boolean formula. In Sixth International Conference on Theory and Applications of Satisfiability Testing, S Margherita Ligure ? Portofino (Italy), May 5?8, 2003. http:\/\/research.microsoft.com\/users\/litaoz\/papers\/SAT_2003_core.pdf"},{"issue":"2","key":"CR24","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/S0166-218X(02)00399-2","volume":"130","author":"Bruni Renato","year":"2003","unstructured":"Renato Bruni. Approximating minimal unsatisfiable sub-formulae by means of adaptive search. Discrete Applied Mathematics, 2003, 130(2): 85?100.","journal-title":"Discrete Applied Mathematics"},{"key":"CR25","unstructured":"Renato Bruni. On exact selection of minimally unsatisfiable subformulae. www.dis.uniroma1.it\/?bruni\/files\/bruni03mus. pdf"},{"key":"CR26","unstructured":"Lingtao Zhang. Zchaff. http:\/\/ee.princeton.edu\/?chaff"},{"key":"CR27","doi-asserted-by":"crossref","unstructured":"Zhang L et al. Conflict driven learning in a quantified Boolean satisfiability solver. In Proc. Int. Conf. Computer Aided Design, San Jose, CA, USA, Nov. 2002, pp. 87?93.","DOI":"10.1145\/774572.774637"},{"key":"CR28","doi-asserted-by":"crossref","unstructured":"Aarti Gupta et al. Iterative abstraction using SAT-based BMC with proof analysis. In Proc. 2003 International Conf. Computer-Aided Design (ICCAD?03), 2003, pp. 416?423.","DOI":"10.1109\/ICCAD.2003.1257811"},{"key":"CR29","doi-asserted-by":"crossref","unstructured":"Renato Bruni et al. Restoring satisfiability or maintaining unsatisfiability by finding small unsatisfiable subformulae. In Proc. Theory and Applications of Satisfiability Testing, Boston, MA, U.S.A. 2001. http:\/\/www.dis.uniroma1.it\/?bruni\/files\/bruni01endm.pdf","DOI":"10.1016\/S1571-0653(04)00320-8"},{"key":"CR30","unstructured":"Holger H Hoos et al. SATLIB: An online resource for research on SAT. In SAT 2000, Gent I P, Maaren H V, Walsh T (eds.), 2000, IOS Press, pp. 283?292. http:\/\/www.satlib.org"}],"container-title":["Journal of Computer Science and Technology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-005-0004-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11390-005-0004-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-005-0004-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,30]],"date-time":"2024-12-30T23:10:03Z","timestamp":1735600203000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11390-005-0004-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,1]]},"references-count":30,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2005,1]]}},"alternative-id":["4"],"URL":"https:\/\/doi.org\/10.1007\/s11390-005-0004-6","relation":{},"ISSN":["1000-9000","1860-4749"],"issn-type":[{"type":"print","value":"1000-9000"},{"type":"electronic","value":"1860-4749"}],"subject":[],"published":{"date-parts":[[2005,1]]}}}