{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T09:26:26Z","timestamp":1729675586936,"version":"3.28.0"},"reference-count":29,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015,10]]},"DOI":"10.1109\/emsoft.2015.7318277","type":"proceedings-article","created":{"date-parts":[[2015,11,9]],"date-time":"2015-11-09T17:52:50Z","timestamp":1447091570000},"page":"217-226","source":"Crossref","is-referenced-by-count":10,"title":["Automatic verification of linear controller software"],"prefix":"10.1109","author":[{"given":"Miroslav","family":"Pajic","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Junkil","family":"Park","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Insup","family":"Lee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"George J.","family":"Pappas","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Oleg","family":"Sokolsky","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/EMSOFT.2013.6658600"},{"key":"ref11","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":"Tools and Algorithms for the Construction and Analysis of Systems"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1145\/2480362.2480593"},{"journal-title":"A Discipline of Programming","year":"1976","author":"dijkstra","key":"ref13"},{"key":"ref14","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3290-0","author":"dullerud","year":"2000","journal-title":"A Course in Robust Control Theory"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2014.2341931"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/MCS.2010.938196"},{"journal-title":"Linear Robust Control","year":"2012","author":"green","key":"ref17"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14261-1_15"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28891-3_15"},{"key":"ref28","article-title":"From design to implementation: an automated, credible autocoding chain for control systems","author":"wang","year":"2013","journal-title":"arXiv preprint arXiv 1307 2641"},{"journal-title":"The Coq Proof Assistant Reference Manual - Version 8 1","year":"1997","author":"barras","key":"ref4"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2007.344"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/CONTROL.2014.6915147"},{"journal-title":"ACSL ANSI\/ISO C Specification Language Version 1 4 Technical report CEA LIST and INRIA","year":"2010","author":"baudin","key":"ref6"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1109\/ACC.2014.6859131"},{"journal-title":"WP 0 8 manual-Frama-C Technical report CEA LIST","year":"2014","author":"baudin","key":"ref5"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06200-6_29"},{"key":"ref7","first-page":"53","article-title":"Why 3: Shepherd your herd of provers","author":"bobot","year":"2011","journal-title":"Boogie 2011 First International Workshop on Intermediate Verification Languages"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/1879021.1879024"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33826-7_16"},{"journal-title":"The WhyML Programming Language","year":"0","key":"ref1"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28891-3_33"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40787-1_29"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1145\/2380356.2380380"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2013.6760105"},{"journal-title":"Linear System Theory","year":"1996","author":"rugh","key":"ref26"},{"key":"ref25","first-page":"543","article-title":"Static Analysis of the XEN Kernel using Frama-C","volume":"16","author":"puccetti","year":"2010","journal-title":"Journal of Universal Computer Science"}],"event":{"name":"2015 International Conference on Embedded Software (EMSOFT)","start":{"date-parts":[[2015,10,4]]},"location":"Amsterdam, Netherlands","end":{"date-parts":[[2015,10,9]]}},"container-title":["2015 International Conference on Embedded Software (EMSOFT)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/7313572\/7318008\/07318277.pdf?arnumber=7318277","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,23]],"date-time":"2017-06-23T19:14:41Z","timestamp":1498245281000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7318277\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,10]]},"references-count":29,"URL":"https:\/\/doi.org\/10.1109\/emsoft.2015.7318277","relation":{},"subject":[],"published":{"date-parts":[[2015,10]]}}}