{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T22:36:48Z","timestamp":1648679808474},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2010,2,5]],"date-time":"2010-02-05T00:00:00Z","timestamp":1265328000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Electron Test"],"published-print":{"date-parts":[[2010,4]]},"DOI":"10.1007\/s10836-010-5143-1","type":"journal-article","created":{"date-parts":[[2010,2,4]],"date-time":"2010-02-04T11:19:44Z","timestamp":1265282384000},"page":"243-259","source":"Crossref","is-referenced-by-count":0,"title":["Learning from Constraints for Formal Property Checking"],"prefix":"10.1007","volume":"26","author":[{"given":"In-Ho","family":"Moon","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kevin","family":"Harer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,2,5]]},"reference":[{"key":"5143_CR1","series-title":"LNCS","first-page":"193","volume-title":"Fifth international conference on tools and algorithms for construction and analysis of systems (TACAS\u201999)","author":"A Biere","year":"1999","unstructured":"Biere A, Cimatti A, Clarke E, Zhu Y (1999) Symbolic model checking without BDDs. In: Fifth international conference on tools and algorithms for construction and analysis of systems (TACAS\u201999). LNCS, vol 1579. Amsterdam, The Netherlands, pp 193\u2013207"},{"key":"5143_CR2","doi-asserted-by":"crossref","unstructured":"Bjesse P, Claessen K (2000) SAT-based verification without state space traversal. In: Hunt Jr WA, Johnson SD (eds) Formal methods in computer aided design. LNCS, vol 1954. Springer-Verlag, pp 372\u2013389","DOI":"10.1007\/3-540-40922-X_23"},{"key":"5143_CR3","unstructured":"Burch JR, Clarke EM, Long DE (1991) Symbolic model checking with partitioned transition relations. In: In international conference on very large scale integration. North-Holland, pp 49\u201358"},{"key":"5143_CR4","doi-asserted-by":"crossref","unstructured":"Coudert O, Madre JC (1990) A unified framework for the formal verification of sequential circuits. In: Proceedings of the international conference on computer-aided design, pp 126\u2013129","DOI":"10.1109\/ICCAD.1990.129859"},{"key":"5143_CR5","doi-asserted-by":"crossref","unstructured":"Een N, Biere A (2005) Effective preprocessing in SAT through variable and clause elimination. In: International conference on theory and applications of satisfiability testing. LNCS, vol\u00a03569. Springer-Verlag, pp 61\u201375","DOI":"10.1007\/11499107_5"},{"key":"5143_CR6","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 design automation conference, pp 824\u2013829","DOI":"10.1145\/775832.776040"},{"key":"5143_CR7","unstructured":"Ho P-S, Shiple T, Harer K, Kukula J, Damiano R, Bertacco V et al (2000) Smart simulation using collaborative formal and simulation engines. In: Proceedings of the international conference on computer-aided design, pp 120\u2013126"},{"key":"5143_CR8","doi-asserted-by":"crossref","unstructured":"Hu AJ, Dill D (1993) Reducing BDD size by exploiting functional dependencies. In: Proceedings of the design automation conference, pp 266\u2013271","DOI":"10.1145\/157485.164888"},{"key":"5143_CR9","doi-asserted-by":"crossref","unstructured":"Iyer MA (2003) Race: a word-level ATPG-based constraints solver system for smart random simulation. In: International test conference, pp 299\u2013308","DOI":"10.1109\/TEST.2003.1270852"},{"key":"5143_CR10","doi-asserted-by":"crossref","unstructured":"Kitchen N, Kuehlmann A (2007) Stimulus generation for constrained random simulation. In: Proceedings of the international conference on computer-aided design, pp 258\u2013265","DOI":"10.1109\/ICCAD.2007.4397275"},{"key":"5143_CR11","doi-asserted-by":"crossref","unstructured":"Kukula JH, Shiple TR (2000) Building circuits from relations. In: International computer aided verification conference(CAV\u201900). LNCS, vol\u00a01855. Springer-Verlag, pp 131\u2013143","DOI":"10.1007\/10722167_12"},{"key":"5143_CR12","unstructured":"Lee C, Jiang CHJ, Mishchenko A (2007) Scalable exploitation of functional dependency by interpolation and incremental SAT solving. In: Proceedings of the international conference on computer-aided design, pp 227\u2013233"},{"key":"5143_CR13","volume-title":"Symbolic model checking","author":"KL McMillan","year":"1994","unstructured":"McMillan KL (1994) Symbolic model checking. Kluwer Academic Publishers, Boston, MA"},{"key":"5143_CR14","unstructured":"McMillan K (2000) Interpolation and SAT-based model checking. In: International computer aided verification conference(CAV\u201903). LNCS, vol 2725. Springer-Verlag, pp 1\u201313"},{"key":"5143_CR15","doi-asserted-by":"crossref","unstructured":"Mony H, Baumgartner J, Aziz A (2005) Exploiting constraints in transformation-based verification. In: Correct hardware design and verification methods. LNCS, vol 3725. Springer-Verlag, pp 269\u2013284","DOI":"10.1007\/11560548_21"},{"key":"5143_CR16","unstructured":"Moon I-H, Jang J-Y, Hachtel GD, Somenzi F, Pixley C, Yuan\u00a0J (1998) Approximate reachability don\u2019t cares for CTL model checking. In: Proceedings of the international conference on computer-aided design. San Jose, CA, pp 351\u2013358"},{"key":"5143_CR17","unstructured":"Moon I-H, Kukula J, Shiple T, Somenzi F (1999) Least fixpoint approximations for reachability analysis. In: Proceedings of the international conference on computer-aided design, pp 41\u201344"},{"key":"5143_CR18","unstructured":"Somenzi F CUDD: http:\/\/vlsi.colorado.edu\/~fabio\/CUDD"},{"key":"5143_CR19","doi-asserted-by":"crossref","unstructured":"Wang D, Ho P-H, Long J, Kukula J, Zhu Y, Ma T et\u00a0al (2001) Formal property verification by abstraction refinement with formal, simulation and hybrid engines. In: Proceedings of the design automation conference, pp 35\u201340","DOI":"10.1145\/378239.378260"},{"key":"5143_CR20","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1007\/3-540-48683-6_29","volume-title":"Eleventh conference on computer aided verification (CAV\u201999)","author":"B Yang","year":"1999","unstructured":"Yang B, Simmons R, Bryant RE, O\u2019Hallaron DR (1999) Optimizing symbolic model checking for constraint-rich models. In: Halbwachs N, Peled D (eds) Eleventh conference on computer aided verification (CAV\u201999). LNCS, vol 1633. Springer-Verlag, Berlin, pp 328\u2013340"},{"key":"5143_CR21","doi-asserted-by":"crossref","unstructured":"Yuan J, Shultz K, Pixley C, Miller H, Aziz A (1999) Modeling design constraints and biasing in simulation using BDDs. In: Proceedings of the international conference on computer-aided design, pp 584\u2013589","DOI":"10.1109\/ICCAD.1999.810715"},{"key":"5143_CR22","unstructured":"Zhu Y, Kukula JH (2003) Generator-based verification. In: Proceedings of the international conference on computer-aided design, pp 146\u2013153"}],"container-title":["Journal of Electronic Testing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10836-010-5143-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10836-010-5143-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10836-010-5143-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T01:57:45Z","timestamp":1559267865000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10836-010-5143-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,2,5]]},"references-count":22,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2010,4]]}},"alternative-id":["5143"],"URL":"https:\/\/doi.org\/10.1007\/s10836-010-5143-1","relation":{},"ISSN":["0923-8174","1573-0727"],"issn-type":[{"value":"0923-8174","type":"print"},{"value":"1573-0727","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,2,5]]}}}