{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,28]],"date-time":"2025-05-28T10:45:19Z","timestamp":1748429119904,"version":"3.28.0"},"reference-count":38,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1109\/memcod.2005.1487900","type":"proceedings-article","created":{"date-parts":[[2005,7,27]],"date-time":"2005-07-27T17:52:28Z","timestamp":1122486748000},"page":"101-110","source":"Crossref","is-referenced-by-count":59,"title":["Formal verification of SystemC by automatic hardware\/software partitioning"],"prefix":"10.1109","author":[{"given":"D.","family":"Kroening","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"N.","family":"Sharygina","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"19","doi-asserted-by":"publisher","DOI":"10.1109\/DSD.2002.1115387"},{"journal-title":"The Theory and Practice of Concurrency","year":"1997","author":"roscoe","key":"35"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1007\/11925040_7"},{"key":"36","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36135-9_25"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1145\/337292.337339"},{"key":"33","doi-asserted-by":"publisher","DOI":"10.1145\/201019.201032"},{"key":"15","article-title":"Synthesis of synchronization skeletons for branching time temporal logic","volume":"131","author":"clarke","year":"1981","journal-title":"LNCS"},{"key":"34","doi-asserted-by":"publisher","DOI":"10.1007\/BF00936948"},{"key":"16","first-page":"293","article-title":"Generating finite-state abstractions of reactive systems using decision procedures","volume":"1427","author":"colo?n","year":"1998","journal-title":"LNCS"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1023\/B:FORM.0000040025.89719.f3"},{"key":"14","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-540-31980-1_40","article-title":"SATABS: SAT-based predicated abstraction for ANSIC","author":"clarke","year":"2005","journal-title":"Proceedings of the 11th International Conf on Tools and Algorithms for Construction and Analysis of Systems (TACAS)"},{"year":"0","key":"37"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2003.1210089"},{"key":"38","doi-asserted-by":"publisher","DOI":"10.1109\/ASPDAC.2004.1337573"},{"key":"12","article-title":"Predicate abstraction and refinement techniques for verifying verilog","volume":"cmu cs 4 139","author":"clarke","year":"2004","journal-title":"Technical Report"},{"key":"21","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"20","first-page":"72","article-title":"Construction of abstract state graphs with PVS","volume":"1254","author":"graf","year":"1997","journal-title":"LNCS"},{"key":"22","article-title":"Overview of ComFoRT, a model checking reasoning framework","author":"ivers","year":"2004","journal-title":"Technical Report"},{"key":"23","first-page":"7","article-title":"Verification of SpecC and Verilog using predicate abstraction","author":"jain","year":"2004","journal-title":"Proceedings of MEMOCODE 2004"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1145\/1065579.1065697"},{"key":"25","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1007\/3-540-69108-1_20","article-title":"ESTL: A temporal logic for events and states","volume":"1420","author":"kindler","year":"1998","journal-title":"Lecture Notes in Computer Science"},{"key":"26","doi-asserted-by":"publisher","DOI":"10.1109\/ICCAD.2004.1382544"},{"key":"27","first-page":"368","article-title":"Behavioral consistency of C and Verilog programs using bounded model checking","author":"kroening","year":"2003","journal-title":"Proc DAC 2003"},{"key":"28","doi-asserted-by":"crossref","first-page":"298","DOI":"10.1007\/3-540-36384-X_24","article-title":"Efficient computation of recurrence diameters","volume":"2575","author":"kroening","year":"2003","journal-title":"Lecture Notes in Computer Science"},{"key":"29","article-title":"HardwareC - A language for hardware design (version 2.0)","volume":"csl tr 90 419","author":"ku","year":"1990","journal-title":"Technical Report"},{"key":"3","article-title":"Boolean programs: A model and process for software analysis","volume":"2000","author":"ball","year":"2000","journal-title":"Technical Report"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1145\/318593.318638"},{"journal-title":"Model checking","year":"1999","author":"clarke","key":"10"},{"year":"0","key":"1"},{"key":"30","doi-asserted-by":"publisher","DOI":"10.1515\/9781400864041"},{"key":"7","article-title":"State\/event-based software model checking","volume":"2999","author":"clarke","year":"2004","journal-title":"Proceedings of the International Conf on Integrated Formal Methods LNCS"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2003.1201217"},{"key":"32","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.2001.156196"},{"key":"5","first-page":"193","article-title":"Symbolic model checking without BDDs","author":"biere","year":"1999","journal-title":"TACAS"},{"key":"31","article-title":"Enhancing formal methods for SystemC designs","author":"man","year":"2003","journal-title":"PROGRESS 2003 Embedded Systems Symposium"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.1999.781333"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143235"},{"key":"8","first-page":"154","article-title":"Counterexample-guided abstraction refinement","author":"clarke","year":"2000","journal-title":"CAV"}],"event":{"name":"Third ACM & amp; IEEE International Conference on Formal Methods and Models for Co-Design","acronym":"MEMCOD-05","location":"Verona, Italy"},"container-title":["Proceedings. Second ACM and IEEE International Conference on Formal Methods and Models for Co-Design, 2005. MEMOCODE '05."],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/9956\/32009\/01487900.pdf?arnumber=1487900","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,16]],"date-time":"2017-06-16T21:36:14Z","timestamp":1497648974000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1487900\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":38,"URL":"https:\/\/doi.org\/10.1109\/memcod.2005.1487900","relation":{},"subject":[]}}