{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T12:02:05Z","timestamp":1725710525040},"reference-count":23,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012,7]]},"DOI":"10.1109\/memcod.2012.6292294","type":"proceedings-article","created":{"date-parts":[[2012,9,10]],"date-time":"2012-09-10T19:45:06Z","timestamp":1347306306000},"page":"1-10","source":"Crossref","is-referenced-by-count":6,"title":["Compositional performance verification of NoC designs"],"prefix":"10.1109","author":[{"given":"Daniel E.","family":"Holcomb","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Gotmanov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Kishinevsky","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sanjit A.","family":"Seshia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"19","doi-asserted-by":"publisher","DOI":"10.1145\/1269843.1269846"},{"key":"22","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2012.6176626"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1109\/MDT.2005.99"},{"key":"23","article-title":"Checking a large routine","author":"turing","year":"0","journal-title":"Conference on High Speed Automatic Calculating Machines 1949"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1109\/18.61109"},{"article-title":"Method and apparatus for synchronous unbuffered flow control of packets on a ring interconnect","year":"2009","author":"mattina","key":"15"},{"article-title":"Method and apparatus for preventing starvation in a slotted-ring network","year":"2010","author":"mattina","key":"16"},{"key":"13","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-14295-6_5","article-title":"ABC: An Academic Industrial- Strength Verification Tool","author":"brayton","year":"2010","journal-title":"Computer Aided Verification"},{"journal-title":"Principles and Practices of Interconnection Networks","year":"0","author":"dally","key":"14"},{"key":"11","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-18275-4_16","article-title":"Verifying Deadlock-Freedom of Communication Fabrics","author":"gotmanov","year":"2011","journal-title":"Verification Model Checking and Abstract Interpretation"},{"key":"12","article-title":"Enhancing ABC for LTL Stabilization Verification of SystemVerilog\/VHDL Models","author":"long","year":"0","journal-title":"International Workshop on Design and Implementation of Formal Tools and Systems 2011"},{"key":"21","article-title":"Hunting deadlocks efficiently in microarchitectural models of communication fabrics","author":"verbeek","year":"2011","journal-title":"Formal Methods in Computer-Aided Design"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1109\/MM.2009.9"},{"key":"20","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80410-9"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1147\/rd.515.0559"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.1109\/MM.2007.4378780"},{"key":"10","article-title":"Efficient implementation of property directed reachability","author":"een","year":"0","journal-title":"Proceedings of International Workshop on Logic Synthesis 2011"},{"key":"7","first-page":"108","article-title":"Checking safety properties using induction and a SAT-solver","author":"sheeran","year":"2000","journal-title":"Formal Methods in Computer-Aided Design"},{"key":"6","article-title":"Abstraction-Based Performance Analysis of NoCs","author":"holcomb","year":"0","journal-title":"Design Automation Conference Jun 2011"},{"key":"5","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-14295-6_29","article-title":"Automatic Generation of Inductive Invariants from High-Level Microarchitectural Models of Communication Fabrics","author":"chatterjee","year":"2010","journal-title":"Computer Aided Verification"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1109\/HLDVT.2010.5496662"},{"key":"9","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-18275-4_7","article-title":"SAT-Based Model Checking Without Unrolling","author":"bradley","year":"2011","journal-title":"Verification Model Checking and Abstract Interpretation"},{"key":"8","first-page":"1","article-title":"Interpolation and SAT-based model checking","author":"mcmillan","year":"2003","journal-title":"Computer Aided Verification"}],"event":{"name":"2012 10th IEEE\/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE 2012)","start":{"date-parts":[[2012,7,16]]},"location":"Arlington, VA, USA","end":{"date-parts":[[2012,7,17]]}},"container-title":["Tenth ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMCODE2012)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/6287679\/6292291\/06292294.pdf?arnumber=6292294","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,3]],"date-time":"2019-07-03T17:58:48Z","timestamp":1562176728000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6292294\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,7]]},"references-count":23,"URL":"https:\/\/doi.org\/10.1109\/memcod.2012.6292294","relation":{},"subject":[],"published":{"date-parts":[[2012,7]]}}}