{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,20]],"date-time":"2026-02-20T19:05:06Z","timestamp":1771614306618,"version":"3.50.1"},"reference-count":39,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"11","license":[{"start":{"date-parts":[[2022,11,1]],"date-time":"2022-11-01T00:00:00Z","timestamp":1667260800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft (DFG), as part of the Collaborative Research Center","doi-asserted-by":"publisher","award":["SFB876"],"award-info":[{"award-number":["SFB876"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100010663","name":"European Research Council (ERC) under the European Union\u2019s Horizon 2020 Research and Innovation Programme through the Project PropRT","doi-asserted-by":"publisher","award":["865170"],"award-info":[{"award-number":["865170"]}],"id":[{"id":"10.13039\/100010663","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."],"published-print":{"date-parts":[[2022,11]]},"DOI":"10.1109\/tcad.2022.3197501","type":"journal-article","created":{"date-parts":[[2022,8,9]],"date-time":"2022-08-09T20:37:03Z","timestamp":1660077423000},"page":"4157-4168","source":"Crossref","is-referenced-by-count":4,"title":["Formal Verification of Resource Synchronization Protocol Implementations: A Case Study in RTEMS"],"prefix":"10.1109","volume":"41","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9879-1394","authenticated-orcid":false,"given":"Junjie","family":"Shi","sequence":"first","affiliation":[{"name":"Design Automation for Embedded Systems Group, TU Dortmund University, Dortmund, Germany"}]},{"given":"Christoph-Cordt","family":"von Egidy","sequence":"additional","affiliation":[{"name":"Design Automation for Embedded Systems Group, TU Dortmund University, Dortmund, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7110-921X","authenticated-orcid":false,"given":"Kuan-Hsun","family":"Chen","sequence":"additional","affiliation":[{"name":"Chair of Computer Architecture and Embedded Systems, University of Twente, Enschede, The Netherlands"}]},{"given":"Jian-Jia","family":"Chen","sequence":"additional","affiliation":[{"name":"Design Automation for Embedded Systems Group, TU Dortmund University, Dortmund, Germany"}]}],"member":"263","reference":[{"key":"ref1","volume-title":"An SMT solver for software verification.","year":"2022"},{"key":"ref2","volume-title":"Frama-C software analyzers.","year":"2022"},{"key":"ref3","volume-title":"The Coq proof assistant","year":"2022"},{"key":"ref4","volume-title":"The source code of this work","year":"2022"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15057-9_3"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2015.35"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/3360573"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/BF00365393"},{"key":"ref9","volume-title":"WP Plug-In Manual, Version 22.0","author":"Baudin","year":"2020"},{"key":"ref10","volume-title":"ACSL: ANSI\/ISO C Specification Language, Version 1.16 for Frama-C 22.0","author":"Baudin","year":"2020"},{"key":"ref11","volume-title":"Introduction to C Program Proof With Frama-C and Its WP Plugin","author":"Blanchard","year":"2020"},{"key":"ref12","first-page":"53","article-title":"Why3: Shepherd your herd of provers","volume-title":"Proc. Boogie 1st Int. Workshop Intermediate Verif. Lang.","author":"Bobot"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/ECRTS.2013.37"},{"key":"ref14","volume-title":"Real-Time Systems and Programming Languages\u2014Ada, Real-Time Java and C\/Real-Time POSIX","author":"Burns","year":"2009"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4614-0676-1"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-19584-1_12"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679402"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2018.00057"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_2"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06200-6_17"},{"key":"ref21","volume-title":"Frama-C User Manual, Version 22.0 (Titanium)","author":"Correnson","year":"2020"},{"key":"ref22","first-page":"233","article-title":"Frama-C\u2014A software analysis perspective","volume-title":"Proc. Int. Conf. Softw. Eng. Formal Methods","author":"Cuoq"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03421-4_15"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47846-3_26"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.23943\/princeton\/9780691181301.001.0001"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-60588-3_5"},{"key":"ref28","first-page":"653","article-title":"Certikos: An extensible architecture for building certified concurrent OS kernels","volume-title":"Proc. 12th USENIX Symp. Oper. Syst. Des. Implement. (OSDI)","author":"Gu"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/WSTFES.2003.1201367"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-05089-3_51"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45937-5_16"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS52030.2021.00011"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1109\/ICDCS.1990.89257"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1109\/REAL.1988.51121"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1109\/12.57058"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS.2019.00031"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_11"}],"container-title":["IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/43\/9928799\/09852753.pdf?arnumber=9852753","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,2]],"date-time":"2024-03-02T04:42:13Z","timestamp":1709354533000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/9852753\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,11]]},"references-count":39,"journal-issue":{"issue":"11"},"URL":"https:\/\/doi.org\/10.1109\/tcad.2022.3197501","relation":{},"ISSN":["0278-0070","1937-4151"],"issn-type":[{"value":"0278-0070","type":"print"},{"value":"1937-4151","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,11]]}}}