{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,22]],"date-time":"2024-10-22T20:29:28Z","timestamp":1729628968597,"version":"3.28.0"},"reference-count":46,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012,7]]},"DOI":"10.1109\/memcod.2012.6292302","type":"proceedings-article","created":{"date-parts":[[2012,9,10]],"date-time":"2012-09-10T19:45:06Z","timestamp":1347306306000},"page":"75-84","source":"Crossref","is-referenced-by-count":1,"title":["Interactive verification of synchronous systems"],"prefix":"10.1109","author":[{"given":"Manuel","family":"Gesell","sequence":"first","affiliation":[]},{"given":"Klaus","family":"Schneider","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"19","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-5983-1"},{"key":"35","first-page":"314","article-title":"Proving the equivalence of microstep and macrostep semantics","volume":"2410","author":"schneider","year":"2002","journal-title":"LNCS"},{"key":"17","first-page":"153","article-title":"Why higher-order logic is a good formalism for specifying and verifying hardware","author":"gordon","year":"1986","journal-title":"Formal Aspects of VLSI Design"},{"journal-title":"The Synchronous Programming Language Quartz","year":"2009","author":"schneider","key":"36"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1995.523251"},{"key":"33","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541"},{"key":"15","first-page":"137","article-title":"An overview of LP, the larch power","volume":"355","author":"garland","year":"1989","journal-title":"LNCS"},{"key":"34","doi-asserted-by":"publisher","DOI":"10.1109\/CSD.2001.981772"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1145\/2103776.2103782"},{"key":"39","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63475-4_3"},{"key":"13","first-page":"390","article-title":"The Murphi verification system","volume":"1102","author":"dill","year":"1996","journal-title":"LNCS"},{"key":"14","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","article-title":"Assigning meanings to programs","volume":"19","author":"floyd","year":"1967","journal-title":"Symposia in Applied Mathematics"},{"key":"37","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.02.028"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1145\/62882.62926"},{"key":"38","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-63475-4_6"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"21","doi-asserted-by":"publisher","DOI":"10.1007\/BF00121125"},{"key":"20","article-title":"25 Years of Model Checking - History, Achievements, Perspectives","volume":"5000","author":"grumberg","year":"2008","journal-title":"LNCS"},{"key":"43","doi-asserted-by":"publisher","DOI":"10.1007\/BF01384501"},{"key":"42","doi-asserted-by":"publisher","DOI":"10.1007\/BF01941138"},{"key":"41","first-page":"277","article-title":"Mechanized verification of circuit descriptions using the Larch Prover","author":"staunstrup","year":"1992","journal-title":"Theorem Provers in Circuit Design (TPCD '94)"},{"key":"40","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-52148-8_29"},{"key":"45","first-page":"1","article-title":"A brief survey of program slicing","volume":"30","author":"xu","year":"2005","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"key":"44","first-page":"121","article-title":"A survey of program slicing techniques","volume":"3","author":"tip","year":"1995","journal-title":"Journal of Programming Languages"},{"key":"46","doi-asserted-by":"publisher","DOI":"10.1007\/BF00464355"},{"key":"22","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"journal-title":"Communicating Sequential Processes","year":"1985","author":"hoare","key":"23"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2004.833614"},{"key":"25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_4"},{"key":"26","doi-asserted-by":"publisher","DOI":"10.1145\/307988.307989"},{"key":"27","doi-asserted-by":"publisher","DOI":"10.1007\/BF01383880"},{"journal-title":"A methodology for hardware verification using compositional model checking","year":"1999","author":"mcmillan","key":"28"},{"key":"29","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-59047-1_52"},{"key":"3","first-page":"216","article-title":"Control dependence for extended finite state machines","volume":"5503","author":"androutsopoulos","year":"2009","journal-title":"LNCS"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008739929481"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881"},{"key":"30","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-6315-9_12"},{"journal-title":"The Constructive Semantics of Pure Esterel","year":"1999","author":"berry","key":"7"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2002.805826"},{"key":"32","first-page":"748","article-title":"PVS: A prototype verification system","volume":"607","author":"owre","year":"1992","journal-title":"LNCS"},{"key":"5","first-page":"249","article-title":"Bluespec: A language for hardware design, simulation, synthesis and verification invited talk","author":"arvind","year":"2003","journal-title":"Proc Formal Methods Models Co-Des (MEMOCODE)"},{"key":"31","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360224"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1145\/357146.357150"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1007\/BF01383872"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008700623084"}],"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\/06292302.pdf?arnumber=6292302","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,20]],"date-time":"2017-06-20T23:58:59Z","timestamp":1498003139000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6292302\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,7]]},"references-count":46,"URL":"https:\/\/doi.org\/10.1109\/memcod.2012.6292302","relation":{},"subject":[],"published":{"date-parts":[[2012,7]]}}}