{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:21:15Z","timestamp":1779074475558,"version":"3.51.4"},"reference-count":21,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016,10]]},"DOI":"10.1109\/fmcad.2016.7886662","type":"proceedings-article","created":{"date-parts":[[2017,3,28]],"date-time":"2017-03-28T02:52:44Z","timestamp":1490669564000},"page":"65-72","source":"Crossref","is-referenced-by-count":9,"title":["Efficient uninterpreted function abstraction and refinement for word-level model checking"],"prefix":"10.1109","author":[{"given":"Yen-Sheng","family":"Ho","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pankaj","family":"Chauhan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pritam","family":"Roy","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan","family":"Mishchenko","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert","family":"Brayton","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","article-title":"Boolector: An efficient smt solver for bit-vectors and arrays","author":"brummayer","year":"0","journal-title":"Proc of TACAS'09"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2003.1214874"},{"key":"ref13","article-title":"Z3: An efficient smt solver","author":"de moura","year":"0","journal-title":"Proceedings of TACAS'08"},{"key":"ref14","article-title":"Efficient implementation of property directed reachability","author":"e\u00e9n","year":"0","journal-title":"Proc of FMCAD’ 11"},{"key":"ref15","article-title":"An extensible sat-solver","author":"e\u00e9n","year":"0","journal-title":"Proceedings of SAT '03"},{"key":"ref16","article-title":"Construction of abstract state graphs with pvs","author":"graf","year":"0","journal-title":"Proc of CAV'97"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/1065579.1065697"},{"key":"ref18","author":"kroening","year":"0","journal-title":"Ebmc The enhanced bounded model checker"},{"key":"ref19","article-title":"Interpolation and sat-based model checking","author":"mcmillan","year":"0","journal-title":"Proc of CAV'03"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.21236\/ADA360973"},{"key":"ref3","article-title":"The SMT-LIB Standard: Version 2.0. Technical report, Department of Computer Science","author":"barrett","year":"2010","journal-title":"The University of Iowa"},{"key":"ref6","article-title":"Learning conditional abstractions","author":"brady","year":"0","journal-title":"in Proc of FMCAD’10"},{"key":"ref5","article-title":"Sat-based model checking without unrolling","author":"bradley","year":"0","journal-title":"Proc of VMCAI'11"},{"key":"ref8","article-title":"Using speculation for sequential equivalence checking","author":"brayton","year":"0","journal-title":"Proc of IWLS’ 12"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2010.5558624"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/996566.996629"},{"key":"ref1","article-title":"Reveal: A formal verification tool for verilog designs","author":"andraus","year":"0","journal-title":"Proc of LPAR'08"},{"key":"ref9","article-title":"Abc: An academic industrial-strength verification tool","author":"brayton","year":"0","journal-title":"Proc CAV'10"},{"key":"ref20","article-title":"A toolbox for counter-example analysis and optimization","author":"mishchenko","year":"0","journal-title":"Proc of IWLS'13"},{"key":"ref21","article-title":"Checking safety properties using induction and a sat-solver","author":"sheeran","year":"0","journal-title":"Proc FMCAD'00"}],"event":{"name":"2016 16th Conference on Formal Methods in Computer-Aided Design (FMCAD)","location":"Mountain View, CA","start":{"date-parts":[[2016,10,3]]},"end":{"date-parts":[[2016,10,6]]}},"container-title":["2016 Formal Methods in Computer-Aided Design (FMCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/7879555\/7886641\/07886662.pdf?arnumber=7886662","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,17]],"date-time":"2020-04-17T04:41:26Z","timestamp":1587098486000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/7886662\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,10]]},"references-count":21,"URL":"https:\/\/doi.org\/10.1109\/fmcad.2016.7886662","relation":{},"subject":[],"published":{"date-parts":[[2016,10]]}}}