{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,22]],"date-time":"2024-10-22T14:55:18Z","timestamp":1729608918365,"version":"3.28.0"},"reference-count":22,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010,7]]},"DOI":"10.1109\/memcod.2010.5558624","type":"proceedings-article","created":{"date-parts":[[2010,8,27]],"date-time":"2010-08-27T14:37:22Z","timestamp":1282919842000},"page":"31-40","source":"Crossref","is-referenced-by-count":7,"title":["ATLAS: Automatic Term-level abstraction of RTL designs"],"prefix":"10.1109","author":[{"given":"Bryan A.","family":"Brady","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Randal E.","family":"Bryant","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sanjit A.","family":"Seshia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John W.","family":"O'Leary","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","first-page":"78","article-title":"Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions","author":"bryant","year":"2002","journal-title":"Proc Computer-Aided Verification (CAV'02) LNCS 2404"},{"journal-title":"Computer Systems A Programmer's Perspective","year":"2002","author":"bryant","key":"ref11"},{"key":"ref12","first-page":"68","article-title":"Automated verification of pipelined microprocessor control","author":"burch","year":"1994","journal-title":"Computer-Aided Verification (CAV '94) LNCS 818"},{"year":"0","author":"competition","key":"ref13"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_42"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/BF00243132"},{"key":"ref16","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-44585-4_35","article-title":"BOOSTER: Speeding up RTL property checking of digital designs through word-level abstraction","author":"johannesen","year":"2001","journal-title":"Computer Aided Verification"},{"key":"ref17","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/978-3-540-45069-6_33","article-title":"Deductive verification of advanced out-of-order microprocessors","volume":"2725","author":"lahiri","year":"2003","journal-title":"Proc 15th International Conference on Computer-Aided Verification (CAV)"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2005.257"},{"journal-title":"Opencores org Usb controller","year":"0","key":"ref19"},{"key":"ref4","first-page":"218","article-title":"Automatic abstraction and verification of verilog models","author":"andraus","year":"2004","journal-title":"Proceedings 41st Design Automation Conference 2004 DAC"},{"journal-title":"CEGAR-based formal hardware verification A case study Technical Report CSE-TR-531-07","year":"2007","author":"andraus","key":"ref3"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_43"},{"key":"ref5","article-title":"Satisfiability modulo theories","volume":"4","author":"barrett","year":"2009","journal-title":"Handbook of Satisfiability"},{"key":"ref8","article-title":"Boolector: An efficient SMT solver for bit-vectors and arrays","author":"brummayer","year":"2009","journal-title":"Proc TACAS"},{"journal-title":"A User's Guide to UCLID Version 0 1","year":"2008","author":"brady","key":"ref7"},{"key":"ref2","first-page":"19","article-title":"Refinement strategies for verification methods based on datapath abstraction","author":"andraus","year":"2006","journal-title":"Proceedings of ASP-DAC"},{"journal-title":"The UCLID Verification System","year":"0","key":"ref1"},{"journal-title":"Term-level verification of a pipelined CISC microprocessor Technical Report CMU-CS-05-195","year":"2005","author":"bryant","key":"ref9"},{"journal-title":"Flow Control and Micro-Architectural Mechanisms for Extending the Performance of Interconnection Networks","year":"2001","author":"peh","key":"ref20"},{"journal-title":"Icarus verilog","year":"0","author":"williams","key":"ref22"},{"journal-title":"Comprehensive Functional Verification The Complete Industry Cycle","year":"2005","author":"wile","key":"ref21"}],"event":{"name":"2010 8th IEEE\/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010)","start":{"date-parts":[[2010,7,26]]},"location":"Grenoble, France","end":{"date-parts":[[2010,7,28]]}},"container-title":["Eighth ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2010)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/5550962\/5558619\/05558624.pdf?arnumber=5558624","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,2]],"date-time":"2019-06-02T11:04:53Z","timestamp":1559473493000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/5558624\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,7]]},"references-count":22,"URL":"https:\/\/doi.org\/10.1109\/memcod.2010.5558624","relation":{},"subject":[],"published":{"date-parts":[[2010,7]]}}}