{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,21]],"date-time":"2026-07-21T14:23:27Z","timestamp":1784643807375,"version":"3.55.0"},"reference-count":56,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"funder":[{"name":"German Research Foundation DFG","award":["Reinhart Koselleck project grant no. DR 287\/23-1"],"award-info":[{"award-number":["Reinhart Koselleck project grant no. DR 287\/23-1"]}]},{"name":"German Research Foundation DFG","award":["research project under grant no. WI 3401\/5-1"],"award-info":[{"award-number":["research project under grant no. WI 3401\/5-1"]}]},{"name":"German Federal Ministry of Education and Research BMBF","award":["Project SPECifIC under grant no. 01IW13001"],"award-info":[{"award-number":["Project SPECifIC under grant no. 01IW13001"]}]},{"name":"Spanish Ministry of Economy and Competitivity","award":["BES-2012-055572"],"award-info":[{"award-number":["BES-2012-055572"]}]},{"name":"Spanish Ministry of Economy and Competitivity","award":["TEC2014-58036-C4-3-R"],"award-info":[{"award-number":["TEC2014-58036-C4-3-R"]}]},{"name":"Siemens AG"},{"DOI":"10.13039\/501100007837","name":"University of Bremen","doi-asserted-by":"crossref","award":["BremenIDEA out project"],"award-info":[{"award-number":["BremenIDEA out project"]}],"id":[{"id":"10.13039\/501100007837","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100007837","name":"University of Bremen","doi-asserted-by":"crossref","award":["Graduate School SyDe"],"award-info":[{"award-number":["Graduate School SyDe"]}],"id":[{"id":"10.13039\/501100007837","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."],"published-print":{"date-parts":[[2016]]},"DOI":"10.1109\/tcad.2016.2611494","type":"journal-article","created":{"date-parts":[[2016,9,20]],"date-time":"2016-09-20T14:22:56Z","timestamp":1474381376000},"page":"1-1","source":"Crossref","is-referenced-by-count":3,"title":["Towards a Verification Flow Across Abstraction Levels: Verifying Implementations Against Their Formal Specification"],"prefix":"10.1109","author":[{"given":"Pablo","family":"Gonzalez-de-Aledo","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8947-3282","authenticated-orcid":false,"given":"Nils","family":"Przigoda","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Robert","family":"Wille","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rolf","family":"Drechsler","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Pablo","family":"Sanchez","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"crossref","first-page":"152","DOI":"10.1007\/978-3-642-21768-5_12","article-title":"Encoding OCL data types for sat-based verification of UML\/OCL models","author":"soeken","year":"2011","journal-title":"Tests and Proof"},{"key":"ref38","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","article-title":"Z3: An efficient SMT solver","author":"de moura","year":"2008","journal-title":"Proc Tools Algorithms Construct Anal Syst"},{"key":"ref33","first-page":"85","author":"gogolla","year":"2002","journal-title":"Expressing UML Class Diagrams Properties With OCL (LNCS)"},{"key":"ref32","year":"2014","journal-title":"Object Constraint Language"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/MODELS.2015.7338257"},{"key":"ref30","doi-asserted-by":"crossref","first-page":"309","DOI":"10.7873\/DATE.2015.0646","article-title":"Assisted generation of frame conditions for formal models","author":"niemann","year":"2015","journal-title":"Proc Design Autom Test Europe"},{"key":"ref37","doi-asserted-by":"crossref","first-page":"481","DOI":"10.1007\/978-3-642-17511-4_27","article-title":"Satisfiability of non-linear (Ir)rational arithmetic","author":"zankl","year":"2010","journal-title":"Logic for Programming Artificial Intelligence and Reasoning"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"ref35","author":"jackson","year":"2006","journal-title":"Software Abstractions–Logic Language and Analysis"},{"key":"ref34","author":"steinberg","year":"2009","journal-title":"EMF Eclipse Modeling Framework 2 0"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/DSD.2015.88"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1145\/2660540.2660981"},{"key":"ref29","author":"barrett","year":"2016","journal-title":"The Satisfiability Modulo Theories Library (SMT-LIB)"},{"key":"ref2","year":"2012","journal-title":"OMG Systems Modeling Language (OMG SysML™)"},{"key":"ref1","author":"rumbaugh","year":"1999","journal-title":"The Unified Modeling Language Reference Manual"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/2463209.2488877"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02949-3_8"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/ICSTW.2008.54"},{"key":"ref24","first-page":"273","article-title":"From application models to filmstrip models: An approach to automatic validation of model dynamics","author":"gogolla","year":"2014","journal-title":"Proc Modellierung"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2010.5457017"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04425-0_52"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00255-7_4"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68237-0_23"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2012.6176655"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.7873\/DATE.2013.022"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2012.2188800"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.1007\/978-90-481-9255-7"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1142\/S0218126616400211"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1109\/DDECS.2015.52"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45669-4_13"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/DATE.2011.5763177"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2004.1281665"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/MODELS.2015.7338248"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1145\/2976767.2976780"},{"key":"ref14","first-page":"53","article-title":"Formal specification level: Towards verification-driven design based on natural language processing","author":"drechsler","year":"2012","journal-title":"Proc Forum Spec Design Lang"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/1966445.1966463"},{"key":"ref16","first-page":"209","article-title":"KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs","author":"cadar","year":"2008","journal-title":"Proc USENIX Symp on Operating System Design and Implementation"},{"key":"ref17","doi-asserted-by":"crossref","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","article-title":"A Tool for checking ANSI-C programs","author":"clarke","year":"2004","journal-title":"Proc Tools Algorithms Construct Anal Syst"},{"key":"ref18","doi-asserted-by":"crossref","first-page":"429","DOI":"10.1007\/978-3-662-46681-0_36","article-title":"FramewORk for embedded system verification–(competition contribution)","author":"de aledo","year":"2015","journal-title":"Proc Tools Algorithms Construct Anal Syst"},{"key":"ref19","first-page":"113","article-title":"Proving transaction and system-level properties of untimed SystemC TLM designs","author":"gro\u00dfe","year":"2010","journal-title":"Proc Int Conf Formal Methods Models Codesign"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/b135980"},{"key":"ref3","year":"2011","journal-title":"UML Profile for MARTE Modeling and Analysis of Real-Time Embedded Systems"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1561\/1000000013"},{"key":"ref5","author":"gr\u00f6tker","year":"2002","journal-title":"System Design with SystemC"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.03.017"},{"key":"ref7","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/j.entcs.2004.10.024","article-title":"UML automatic verification tool with formal methods","volume":"127","author":"guti\u00e9rrez","year":"2005","journal-title":"Electron Notes Theor Comput Sci"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1109\/DSD.2012.37"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1016\/j.datak.2011.09.004"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33654-6_3"},{"key":"ref45","author":"peleska","year":"2016","journal-title":"Turn indicator model overview"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1109\/HLDVT.2010.5496658"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21215-9_12"},{"key":"ref42","first-page":"389","article-title":"CBMC–C bounded model checker","author":"kroening","year":"2014","journal-title":"Tools and Algorithms for the Construction and Analysis of Systems"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-29510-7_13"},{"key":"ref44","first-page":"263","article-title":"CUTE: A concolic unit testing engine for C","author":"sen","year":"2005","journal-title":"Proc European Software Eng Conf"},{"key":"ref43","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1145\/1064978.1065036","article-title":"Dart: Directed automated random testing","volume":"40","author":"godefroid","year":"2005","journal-title":"ACM SIGPLAN Notices"}],"container-title":["IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/43\/6917053\/07572163.pdf?arnumber=7572163","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T11:38:10Z","timestamp":1641987490000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7572163\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"references-count":56,"URL":"https:\/\/doi.org\/10.1109\/tcad.2016.2611494","relation":{},"ISSN":["0278-0070","1937-4151"],"issn-type":[{"value":"0278-0070","type":"print"},{"value":"1937-4151","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}