{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T17:36:48Z","timestamp":1762018608838,"version":"build-2065373602"},"reference-count":46,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019,10]]},"DOI":"10.23919\/fmcad.2019.8894264","type":"proceedings-article","created":{"date-parts":[[2019,11,13]],"date-time":"2019-11-13T09:25:06Z","timestamp":1573637106000},"page":"129-137","source":"Crossref","is-referenced-by-count":17,"title":["Shield Synthesis for Real: Enforcing Safety in Cyber-Physical Systems"],"prefix":"10.23919","author":[{"given":"Meng","family":"Wu","sequence":"first","affiliation":[]},{"given":"Jingbo","family":"Wang","sequence":"additional","affiliation":[]},{"given":"Jyotirmoy","family":"Deshmukh","sequence":"additional","affiliation":[]},{"given":"Chao","family":"Wang","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1145\/3178126.3178140"},{"key":"ref38","first-page":"303","article-title":"Enhancing server availability and security through failure-oblivious computing","author":"rinard","year":"2004","journal-title":"USENIX Symposium on Operating Systems Design and Implementation"},{"key":"ref33","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-11494-7_22","article-title":"Specification and verification of concurrent systems in CESAR","author":"quielle","year":"1982","journal-title":"Symposium on Programming"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75293"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1109\/ICCPS.2018.00026"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1145\/3092282.3092296"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-25150-9_31"},{"key":"ref35","first-page":"239","article-title":"Reactive synthesis from signal temporal logic specifications","author":"raman","year":"2015","journal-title":"International Conference on Hybrid Systems Computation and Control"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2014.7039363"},{"key":"ref10","first-page":"121","article-title":"Verifying hyperliveness","author":"coenen","year":"2019","journal-title":"Int'l Conference ComputerAided Verification"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1145\/353323.353382"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11164-3_19"},{"key":"ref13","first-page":"432","article-title":"Verifai: A toolkit for the formal design and analysis of artificial intelligence-based systems","author":"dreossi","year":"2019","journal-title":"International Conference on Computer Aided Verification"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/2562059.2562128"},{"key":"ref15","doi-asserted-by":"crossref","first-page":"178","DOI":"10.1007\/11940197_12","article-title":"Robustness of temporal logic specifications","author":"fainekos","year":"2006","journal-title":"Proc Int'l Workshop Formal Approaches to Testing and Runtime Verification"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-011-0196-8"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1016\/j.ifacol.2015.11.195"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_11"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/2562059.2562140"},{"key":"ref28","article-title":"Infinite games","author":"mazala","year":"2001","journal-title":"Automata Logics and Infinite Games A Guide to Current Research"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/2000799.2000800"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30206-3_12"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_36"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2011.08.007"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1109\/TCST.2015.2501351"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-013-0191-5"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2018.00019"},{"key":"ref7","article-title":"Shield synthesis: Runtime enforcement for reactive systems","author":"bloem","year":"2015","journal-title":"International Conference on Tools and Algorithms for Construction and Analysis of Systems"},{"key":"ref2","first-page":"2669","article-title":"Safe reinforcement learning via shielding","author":"alshiekh","year":"2018","journal-title":"AAAI Conference on Artificial Intelligence"},{"key":"ref9","first-page":"52","article-title":"Design and synthesis of synchronization skeletons using branching time temporal logic","author":"clarke","year":"1981","journal-title":"Logics of Programs"},{"journal-title":"CUDD CU Decision Diagram Package","year":"0","key":"ref1"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2015.2421907"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1145\/2610384.2610405"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985828"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-017-0276-9"},{"key":"ref21","first-page":"443","article-title":"The marabou framework for verification and analysis of deep neural networks","author":"katz","year":"2019","journal-title":"International Conference on Computer Aided Verification"},{"journal-title":"Synthesis of switching protocols from temporal logic specifications","year":"2011","author":"liu","key":"ref24"},{"key":"ref42","first-page":"30:1","article-title":"Reasoning about safety of learning-enabled components in autonomous cyber-physical systems","author":"tuncali","year":"2018","journal-title":"ACM\/IEEE Design Automation Conference"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1145\/1455526.1455532"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-012-0224-3"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/2483760.2483766"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1145\/3061639.3072957"},{"key":"ref25","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1145\/2594291.2594337","article-title":"Automatic runtime error repair and containment via recovery shepherding","author":"long","year":"2014","journal-title":"ACM SIGPLAN conference on Programming Language design and Implementation"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40648-0_6"}],"event":{"name":"2019 Formal Methods in Computer Aided Design (FMCAD)","start":{"date-parts":[[2019,10,22]]},"location":"San Jose, CA, USA","end":{"date-parts":[[2019,10,25]]}},"container-title":["2019 Formal Methods in Computer Aided Design (FMCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/8891869\/8894241\/08894264.pdf?arnumber=8894264","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,2,3]],"date-time":"2021-02-03T01:29:49Z","timestamp":1612315789000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8894264\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10]]},"references-count":46,"URL":"https:\/\/doi.org\/10.23919\/fmcad.2019.8894264","relation":{},"subject":[],"published":{"date-parts":[[2019,10]]}}}