{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T16:30:59Z","timestamp":1773246659261,"version":"3.50.1"},"reference-count":25,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018,10]]},"DOI":"10.23919\/fmcad.2018.8603014","type":"proceedings-article","created":{"date-parts":[[2019,1,9]],"date-time":"2019-01-09T01:33:52Z","timestamp":1546997632000},"page":"1-5","source":"Crossref","is-referenced-by-count":26,"title":["CoSA: Integrated Verification for Agile Hardware Design"],"prefix":"10.23919","author":[{"given":"Cristian","family":"Mattarei","sequence":"first","affiliation":[]},{"given":"Makai","family":"Mann","sequence":"additional","affiliation":[]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[]},{"given":"Ross G.","family":"Daly","sequence":"additional","affiliation":[]},{"given":"Dillon","family":"Huff","sequence":"additional","affiliation":[]},{"given":"Pat","family":"Hanrahan","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61474-5_93"},{"key":"ref11","author":"daly","year":"2017","journal-title":"CoreIR A simple LLVM-style hardware compiler"},{"key":"ref12","first-page":"373","article-title":"Pysmt: a solver-agnostic library for fast prototyping of smt-based algorithms","author":"gario","year":"2015","journal-title":"13th International Workshop on Satisfiability Modulo Theories"},{"key":"ref13","author":"huff","year":"2018","journal-title":"Verilog to CoreIR translator"},{"key":"ref14","author":"mattarei","year":"2018","journal-title":"CoSA CoreIR Symbolic Analyzer"},{"key":"ref15","first-page":"1","article-title":"Interpolation and sat-based model checking","author":"mcmillan","year":"2003","journal-title":"International Conference on Computer Aided Verification"},{"key":"ref16","first-page":"587","article-title":"Btor2, BtorMC and Boolector 3.0","author":"niemetz","year":"2018","journal-title":"Computer Aided Verification - 30th International Conference CAV 2018 Held as Part of the Federated Logic Conference FloC 2018 Oxford UK July 14-17 2018 Proceedings Part I volume 10981 of Lecture Notes in Computer Science"},{"key":"ref17","article-title":"BTOR2, BtorMC and Boolector 3.0","author":"niemetz","year":"2018","journal-title":"Computer Aided Verification - 30th International Conference CAV 2018 Oxford UK July 14-17 Lecture Notes in Computer Science"},{"key":"ref18","author":"parkhurst","year":"2018","journal-title":"AHA Agile Hardware Project"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/2499370.2462176"},{"key":"ref4","first-page":"193","author":"biere","year":"0","journal-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems"},{"key":"ref3","first-page":"825","article-title":"Satisfiability modulo theories","volume":"185","author":"barrett","year":"2009","journal-title":"Handbook of Satisfiability"},{"key":"ref6","article-title":"Aiger 1.9 and beyond","author":"biere","year":"2011","journal-title":"Available at fmv jku at\/hwmcc11\/beyond1 pdf"},{"key":"ref5","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","article-title":"Bounded model checking","volume":"58","author":"biere","year":"2003","journal-title":"Advances in Computers"},{"key":"ref8","first-page":"334","article-title":"The nuxmv symbolic model checker","author":"cavada","year":"2014","journal-title":"International Conference on Computer Aided Verification"},{"key":"ref7","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/978-3-642-14295-6_5","article-title":"Abc: An academic industrial-strength verification tool","author":"brayton","year":"2010","journal-title":"International Conference on Computer Aided Verification"},{"key":"ref2","first-page":"14","article-title":"The smt-lib standard: Version 2.0","volume":"13","author":"barrett","year":"2010","journal-title":"Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh England)"},{"key":"ref9","first-page":"52","article-title":"A liveness checking algorithm that counts","author":"claessen","year":"2012","journal-title":"Formal Methods in Computer-Aided Design (FMCAD)"},{"key":"ref1","first-page":"171","article-title":"Cvc4","author":"barrett","year":"2011","journal-title":"Proceedings of the 23rd International Conference on Computer Aided Verification (CAV ’11) volume 6806 of Lecture Notes in Computer Science"},{"key":"ref20","first-page":"127","article-title":"Checking safety properties using induction and a sat-solver","author":"sheeran","year":"2000","journal-title":"International Conference on Formal Methods In Computer-Aided Design"},{"key":"ref22","doi-asserted-by":"crossref","first-page":"238","DOI":"10.1007\/3-540-60915-6_6","article-title":"An automata-theoretic approach to linear temporal logic","author":"vardi","year":"1996","journal-title":"Logics for Concurrency"},{"key":"ref21","author":"university","year":"2017","journal-title":"Magma a Hardware Design Language Embedded in Python"},{"key":"ref24","year":"0","journal-title":"Verific Design Automation"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2016.7783755"},{"key":"ref25","article-title":"Yosys-a free Verilog synthesis suite","author":"wolf","year":"2013","journal-title":"Proc Austrian Workshop on Microelectronics (Austrochip)"}],"event":{"name":"2018 Formal Methods in Computer Aided Design (FMCAD)","location":"Austin, TX","start":{"date-parts":[[2018,10,30]]},"end":{"date-parts":[[2018,11,2]]}},"container-title":["2018 Formal Methods in Computer Aided Design (FMCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8585253\/8602989\/08603014.pdf?arnumber=8603014","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,26]],"date-time":"2022-01-26T00:16:20Z","timestamp":1643156180000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8603014\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10]]},"references-count":25,"URL":"https:\/\/doi.org\/10.23919\/fmcad.2018.8603014","relation":{},"subject":[],"published":{"date-parts":[[2018,10]]}}}