{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,2]],"date-time":"2026-04-02T15:57:17Z","timestamp":1775145437322,"version":"3.50.1"},"reference-count":34,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"10","license":[{"start":{"date-parts":[[2017,10,1]],"date-time":"2017-10-01T00:00:00Z","timestamp":1506816000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2017,10,1]],"date-time":"2017-10-01T00:00:00Z","timestamp":1506816000000},"content-version":"am","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2017,10,1]],"date-time":"2017-10-01T00:00:00Z","timestamp":1506816000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2017,10,1]],"date-time":"2017-10-01T00:00:00Z","timestamp":1506816000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1136174"],"award-info":[{"award-number":["1136174"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"DARPA","doi-asserted-by":"publisher","award":["FA8750-12-2-0247"],"award-info":[{"award-number":["FA8750-12-2-0247"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"name":"TerraSwarm, one of six centers of STARnet"},{"DOI":"10.13039\/100000028","name":"Semiconductor Research Corporation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000028","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100007245","name":"MARCO","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100007245","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100000185","name":"DARPA","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"name":"ExCAPE: Expeditions in Computer Augmented Program Engineering","award":["1138996"],"award-info":[{"award-number":["1138996"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Automat. Contr."],"published-print":{"date-parts":[[2017,10]]},"DOI":"10.1109\/tac.2017.2676679","type":"journal-article","created":{"date-parts":[[2017,3,1]],"date-time":"2017-03-01T19:12:15Z","timestamp":1488395535000},"page":"4917-4932","source":"Crossref","is-referenced-by-count":272,"title":["Secure State Estimation for Cyber-Physical Systems Under Sensor Attacks: A Satisfiability Modulo Theory Approach"],"prefix":"10.1109","volume":"62","author":[{"given":"Yasser","family":"Shoukry","sequence":"first","affiliation":[]},{"given":"Pierluigi","family":"Nuzzo","sequence":"additional","affiliation":[]},{"given":"Alberto","family":"Puggelli","sequence":"additional","affiliation":[]},{"given":"Alberto L.","family":"Sangiovanni-Vincentelli","sequence":"additional","affiliation":[]},{"given":"Sanjit A.","family":"Seshia","sequence":"additional","affiliation":[]},{"given":"Paulo","family":"Tabuada","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref33","year":"2015"},{"key":"ref32","article-title":"Imhotep-SMT","year":"2015"},{"key":"ref31","doi-asserted-by":"crossref","first-page":"59","DOI":"10.3233\/SAT190075","article-title":"The Sat4j library, release 2.2","volume":"7","author":"berre","year":"2010","journal-title":"J Satisfiability Boolean Modeling Comput"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1145\/1217856.1217859"},{"key":"ref34","article-title":"CVX: MATLAB software for disciplined convex programming, version 1.21","author":"grant","year":"2010"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/ECC.2015.7330811"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/ISIT.2015.7282993"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/ICCPS.2014.6843720"},{"key":"ref13","article-title":"Secure estimation based Kalman filter for cyber-physical systems against adversarial attacks","author":"chang","year":"2015"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2015.7403027"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2014.7039940"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2015.2492159"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1145\/2566468.2566483"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2010.936020"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/TSP.2011.2161300"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2010.2088690"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.2014.6859155"},{"key":"ref27","first-page":"286","author":"gao","year":"0","journal-title":"Proc Int Joint Conf Autom Reason"},{"key":"ref3","first-page":"55","article-title":"Non-invasive spoofing attacks for anti-lock braking systems","author":"shoukry","year":"0","journal-title":"Proc Workshop Cryptographic Hardware Embedded Syst"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/ALLERTON.2009.5394956"},{"key":"ref29","author":"winston","year":"2008","journal-title":"Operations Research Applications and Algorithms"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2014.2350231"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2013.2266831"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2014.2303233"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/1653662.1653666"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.2015.7171098"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2011.67"},{"key":"ref20","volume":"2","author":"blanke","year":"2006","journal-title":"Diagnosis and Fault-Tolerant Control"},{"key":"ref22","first-page":"71","article-title":"CalCS: SMT solving for non-linear convex constraints","author":"nuzzo","year":"0","journal-title":"Proc Formal Methods Comput -Aided Des"},{"key":"ref21","article-title":"Satisfiability modulo theories","author":"barrett","year":"2009","journal-title":"Handbook of Satisfiability"},{"key":"ref24","first-page":"3","article-title":"Imhotep-SMT: A satisfiability modulo theory solver for secure state estimation","author":"shoukry","year":"0","journal-title":"Proceedings of the 8th International Workshop on Satisfiability Modulo Theories"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.2015.7171925"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/1093390.1093393"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/1277548.1277557"}],"container-title":["IEEE Transactions on Automatic Control"],"original-title":[],"link":[{"URL":"http:\/\/ieeexplore.ieee.org\/ielaam\/9\/8049551\/7867816-aam.pdf","content-type":"application\/pdf","content-version":"am","intended-application":"syndication"},{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/9\/8049551\/07867816.pdf?arnumber=7867816","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,4,8]],"date-time":"2022-04-08T18:47:36Z","timestamp":1649443656000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7867816\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,10]]},"references-count":34,"journal-issue":{"issue":"10"},"URL":"https:\/\/doi.org\/10.1109\/tac.2017.2676679","relation":{},"ISSN":["0018-9286","1558-2523"],"issn-type":[{"value":"0018-9286","type":"print"},{"value":"1558-2523","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,10]]}}}