{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T15:51:17Z","timestamp":1770220277872,"version":"3.49.0"},"reference-count":31,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014,10]]},"DOI":"10.1109\/fmcad.2014.6987599","type":"proceedings-article","created":{"date-parts":[[2014,12,31]],"date-time":"2014-12-31T01:00:39Z","timestamp":1419987639000},"page":"83-90","source":"Crossref","is-referenced-by-count":26,"title":["Template-based circuit understanding"],"prefix":"10.1109","author":[{"given":"Adria","family":"Gascon","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pramod","family":"Subramanyan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bruno","family":"Dutertre","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ashish","family":"Tiwari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dejan","family":"Jovanovic","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sharad","family":"Malik","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"19","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1007\/11527695_5","article-title":"Resolve and expand","author":"biere","year":"2005","journal-title":"Theory and Applications of Satisfiability Testing"},{"key":"17","article-title":"Yices 2 manual","author":"dutertre","year":"2014","journal-title":"Computer Science Laboratory SRI International"},{"key":"18","doi-asserted-by":"crossref","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","article-title":"Yices 2.2","volume":"8559","author":"biere","year":"2014","journal-title":"Computer-Aided Verification (CAV'2014) Ser Lecture Notes in Computer Science"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0156-2"},{"key":"16","year":"2014","journal-title":"Online Repository of Benchmarks and Experimental Results"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2013.6691203"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1145\/1806799.1806833"},{"key":"11","doi-asserted-by":"crossref","DOI":"10.1145\/1993498","volume":"2011","author":"hall","year":"2011","journal-title":"Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation PLDI 2011"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06200-6_23"},{"key":"21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21581-0_19"},{"key":"20","article-title":"A comparative study of 2qbf algorithms","author":"ranjan","year":"2004","journal-title":"SAT"},{"key":"22","article-title":"Proceedings 1991 ieee international conference on computer design: Vlsi in computer & processors","volume":"92","year":"1992","journal-title":"ICCD"},{"key":"23","doi-asserted-by":"publisher","DOI":"10.1109\/EDAC.1993.386495"},{"key":"24","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/s100090100039","article-title":"Application of bdds in boolean matching techniques for formal logic combinational verification","volume":"3","author":"mohnke","year":"2001","journal-title":"STTT"},{"key":"25","doi-asserted-by":"publisher","DOI":"10.1023\/A:1016091418702"},{"key":"26","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","article-title":"Z3: An efficient smt solver","volume":"4963","author":"de moura","year":"2008","journal-title":"TACAS Ser Lecture Notes in Computer Science"},{"key":"27","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1007\/978-3-642-31612-8_10","article-title":"Solving qbf with counterexample guided refinement","volume":"7317","author":"janota","year":"2012","journal-title":"SAT Ser Lecture Notes in Computer Science"},{"key":"28","first-page":"71","article-title":"Depqbf: A dependency-Aware qbf solver","volume":"7","author":"lonsing","year":"2010","journal-title":"JSAT"},{"key":"29","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/11532231_27","article-title":"Skizzo: A suite to evaluate and certify qbfs","volume":"3632","author":"benedetti","year":"2005","journal-title":"CADE Ser Lecture Notes in Computer Science"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.7873\/DATE.2013.264"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1109\/ISCAS.2010.5537093"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.1109\/HST.2012.6224325"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0249-7"},{"key":"30","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1007\/978-3-642-22438-6_10","article-title":"Blocked clause elimination for qbf","volume":"6803","author":"biere","year":"2011","journal-title":"CADE Ser Lecture Notes in Computer Science"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.1992.276313"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-9260(98)00014-5"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1109\/54.785838"},{"key":"31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72788-0_28"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1109\/HST.2013.6581568"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008695706493"}],"event":{"name":"2014 Formal Methods in Computer-Aided Design (FMCAD)","location":"Lausanne, Switzerland","start":{"date-parts":[[2014,10,21]]},"end":{"date-parts":[[2014,10,24]]}},"container-title":["2014 Formal Methods in Computer-Aided Design (FMCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6975680\/6987576\/06987599.pdf?arnumber=6987599","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,31]],"date-time":"2023-07-31T06:57:10Z","timestamp":1690786630000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6987599\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,10]]},"references-count":31,"URL":"https:\/\/doi.org\/10.1109\/fmcad.2014.6987599","relation":{},"subject":[],"published":{"date-parts":[[2014,10]]}}}