{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:07:28Z","timestamp":1776305248276,"version":"3.50.1"},"reference-count":37,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014,10]]},"DOI":"10.1109\/memcod.2014.6961855","type":"proceedings-article","created":{"date-parts":[[2014,11,26]],"date-time":"2014-11-26T15:57:36Z","timestamp":1417017456000},"page":"165-174","source":"Crossref","is-referenced-by-count":10,"title":["From visual to logical formalisms for SoC validation"],"prefix":"10.1109","author":[{"given":"Ranan","family":"Fraer","sequence":"first","affiliation":[]},{"given":"Doron","family":"Keren","sequence":"additional","affiliation":[]},{"given":"Zurab","family":"Khasidashvili","sequence":"additional","affiliation":[]},{"given":"Alexander","family":"Novakovsky","sequence":"additional","affiliation":[]},{"given":"Avi","family":"Puder","sequence":"additional","affiliation":[]},{"given":"Eli","family":"Singerman","sequence":"additional","affiliation":[]},{"given":"Eran","family":"Talmor","sequence":"additional","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]},{"given":"Jin","family":"Yang","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"19","first-page":"54","article-title":"On the formal semantics of statecharts","author":"harel","year":"1987","journal-title":"Proc IEEE 5th Symp Logic in Computer Science"},{"key":"35","first-page":"188","article-title":"Formal techniques for SystemC verification","author":"vardi","year":"2007","journal-title":"Proc 44th Design Automation Conference"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1145\/42411.42414"},{"key":"36","article-title":"BPMN modeling and reference guide: Understanding and using BPMN","author":"white","year":"2008","journal-title":"Future Strategies Inc"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1145\/235321.235322"},{"key":"33","article-title":"Workflow modeling: Tools for process improvement and applications development","author":"sharp","year":"2009","journal-title":"Artech House"},{"key":"15","author":"groetker","year":"2002","journal-title":"System Design with SystemC"},{"key":"34","first-page":"471","article-title":"Alternating automata and program verification","author":"vardi","year":"1995","journal-title":"Computer Science Today-Recent Trends and Developments Volume 1000 of Lecture Notes in Computer Science"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"13","first-page":"298","article-title":"Extending formal reasoning with support for hardware diagrams","author":"fisler","year":"1994","journal-title":"2nd Int'l Conf on Theorem Provers in Circuit Design-Theory Practice and Experience Lecture Notes in Computer Science 901"},{"key":"14","first-page":"7","article-title":"A framework for inherent vacuity","author":"fisman","year":"2008","journal-title":"Haifa Verification Conference Volume 5394 of Lecture Notes in Computer Science"},{"key":"37","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1007\/978-3-540-88194-0_22","article-title":"A process semantics for BPMN","author":"wong","year":"2008","journal-title":"Formal Methods and Software Engineering"},{"key":"11","author":"dijkstra","year":"2002","journal-title":"Cooperating sequential processes"},{"key":"12","first-page":"137","article-title":"Integrating hardware\/firmware verification efforts using SystemC high-level models","author":"falk","year":"2010","journal-title":"Methoden und Beschreibungssprachen Zur Modellierung und Verifikation Von Schaltungen und Systemen (MBMV)"},{"key":"21","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679400"},{"key":"20","author":"holzmann","year":"2004","journal-title":"The SPIN Model Checker Primer and Reference Manual"},{"key":"22","doi-asserted-by":"publisher","DOI":"10.1109\/HST.2014.6855571"},{"key":"23","author":"lamport","year":"2002","journal-title":"Specifying Systems The TLA+ Language and Tools for Hardware and Software Engineers"},{"key":"24","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1109\/FAMCAD.2007.33","article-title":"Automating hazard checking in transactionlevel microarchitecture models","author":"mahajan","year":"2007","journal-title":"Proc 7th Int'l Conf Formal Methods in Computer-Aided Design"},{"key":"25","doi-asserted-by":"publisher","DOI":"10.1109\/2.161279"},{"key":"26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00328-8_59"},{"key":"27","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2009.5351126"},{"key":"28","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1007\/3-540-54415-1_49","article-title":"What is in a step: On the semantics of statecharts","author":"pnueli","year":"1991","journal-title":"Proc Int'l Conf on Theoretical Aspects of Computer Software Lecture Notes in Computer Science 526"},{"key":"29","doi-asserted-by":"publisher","DOI":"10.1007\/s10836-013-5411-y"},{"key":"3","first-page":"242","article-title":"High-level specifications: Lessons from industry","author":"batson","year":"2002","journal-title":"Proc 1st Int'l Symp on Formal Methods for Components and Objects Volume 2852 of Lecture Notes in Computer Science"},{"key":"2","article-title":"ESL design and verification: A prescription for electronic system level methodology","author":"martin b bailey","year":"2010","journal-title":"Morgan Kaufmann"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1016\/j.infsof.2008.02.006"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.1145\/2593069.2596692"},{"key":"30","first-page":"1230","article-title":"LTL satisfiability checking","volume":"12","author":"rozier","year":"2010","journal-title":"Int'l J on Software Tools for Technology Transfer"},{"key":"7","author":"clarke","year":"1999","journal-title":"Model checking"},{"key":"6","first-page":"176","article-title":"Progress on the state explosion problem in model checking","author":"clarke","year":"2001","journal-title":"Informatics - 10 Years Back 10 Years Ahead Lecture Notes in Computer Science 2000"},{"key":"32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-10778-2"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1109\/DAC.1999.781333"},{"key":"31","doi-asserted-by":"publisher","DOI":"10.1016\/0169-7552(95)00122-0"},{"key":"4","author":"bening","year":"2001","journal-title":"Principles of Verifiable RTL Design A Functional Coding Style Supporting Verification Processes"},{"key":"9","author":"diaz","year":"2013","journal-title":"Petri Nets Fundamental Models Verification and Applications"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011227529550"}],"event":{"name":"2014 Twelfth ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2014)","location":"Lausanne, Switzerland","start":{"date-parts":[[2014,10,19]]},"end":{"date-parts":[[2014,10,21]]}},"container-title":["2014 Twelfth ACM\/IEEE Conference on Formal Methods and Models for Codesign (MEMOCODE)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6950639\/6961832\/06961855.pdf?arnumber=6961855","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,17]],"date-time":"2019-08-17T17:38:29Z","timestamp":1566063509000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6961855\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,10]]},"references-count":37,"URL":"https:\/\/doi.org\/10.1109\/memcod.2014.6961855","relation":{},"subject":[],"published":{"date-parts":[[2014,10]]}}}