{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:19:17Z","timestamp":1750220357626,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":9,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,5,19]],"date-time":"2021-05-19T00:00:00Z","timestamp":1621382400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["ECCS-2015403"],"award-info":[{"award-number":["ECCS-2015403"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["Research Training Group 2428"],"award-info":[{"award-number":["Research Training Group 2428"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,5,19]]},"DOI":"10.1145\/3457335.3461715","type":"proceedings-article","created":{"date-parts":[[2021,6,29]],"date-time":"2021-06-29T16:10:52Z","timestamp":1624983052000},"page":"29-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Formal verification of hyperproperties for control systems"],"prefix":"10.1145","author":[{"given":"Mahathi","family":"Anand","sequence":"first","affiliation":[{"name":"LMU Munich, Munich, Germany"}]},{"given":"Vishnu","family":"Murali","sequence":"additional","affiliation":[{"name":"University of Colorado"}]},{"given":"Ashutosh","family":"Trivedi","sequence":"additional","affiliation":[{"name":"University of Colorado"}]},{"given":"Majid","family":"Zamani","sequence":"additional","affiliation":[{"name":"University of Colorado Boulder"}]}],"member":"320","published-online":{"date-parts":[[2021,6,29]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"-P. Principles of model checking","author":"Baier C.","year":"2008","unstructured":"Baier , C. , and Katoen , J . -P. Principles of model checking . MIT press , 2008 . Baier, C., and Katoen, J.-P. Principles of model checking. MIT press, 2008."},{"key":"e_1_3_2_1_2_1","volume-title":"Formal methods for discrete-time dynamical systems. Studies in Systems, Decision and Control","author":"Belta C.","year":"2017","unstructured":"Belta , C. , Yordanov , B. , and G\u00d6 L, E . Formal methods for discrete-time dynamical systems. Studies in Systems, Decision and Control . Springer International Publishing , 2017 . Belta, C., Yordanov, B., and G\u00d6L, E. Formal methods for discrete-time dynamical systems. Studies in Systems, Decision and Control. Springer International Publishing, 2017."},{"key":"e_1_3_2_1_3_1","first-page":"265","volume-title":"LNCS","author":"Clarkson M. R.","unstructured":"Clarkson , M. R. , Finkbeiner , B. , Koleini , M. , Micinski , K. K. , Rabe , M. N. , and S\u00e1nchez , C . Temporal logics for hyperproperties. In Principles of Security and Trust (2014) , LNCS , pp. 265 -- 284 . Clarkson, M. R., Finkbeiner, B., Koleini, M., Micinski, K. K., Rabe, M. N., and S\u00e1nchez, C. Temporal logics for hyperproperties. In Principles of Security and Trust (2014), LNCS, pp. 265--284."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/1891823.1891830"},{"key":"e_1_3_2_1_5_1","article-title":"Formal synthesis of stochastic systems via control barrier certificates","author":"Jagtap P.","year":"2020","unstructured":"Jagtap , P. , Soudjani , S. , and Zamani , M . Formal synthesis of stochastic systems via control barrier certificates . IEEE Transactions on Automatic Control ( 2020 ). Jagtap, P., Soudjani, S., and Zamani, M. Formal synthesis of stochastic systems via control barrier certificates. IEEE Transactions on Automatic Control (2020).","journal-title":"IEEE Transactions on Automatic Control ("},{"key":"e_1_3_2_1_6_1","first-page":"1","volume-title":"Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control (New York, NY, USA, 2020), HSCC '20, Association for Computing Machinery","author":"Jagtap P.","unstructured":"Jagtap , P. , Swikir , A. , and Zamani , M . Compositional construction of control barrier functions for interconnected control systems . In Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control (New York, NY, USA, 2020), HSCC '20, Association for Computing Machinery , pp. 1 -- 11 . Jagtap, P., Swikir, A., and Zamani, M. Compositional construction of control barrier functions for interconnected control systems. In Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control (New York, NY, USA, 2020), HSCC '20, Association for Computing Machinery, pp. 1--11."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/LCSYS.2020.3037840"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2002.1184594"},{"key":"e_1_3_2_1_9_1","volume-title":"Using SeDuMi 1.02, a MATLAB toolbox for optimization over symmetric cones. Optimization methods and software 11, 1-4","author":"Sturm J. F.","year":"1999","unstructured":"Sturm , J. F. Using SeDuMi 1.02, a MATLAB toolbox for optimization over symmetric cones. Optimization methods and software 11, 1-4 ( 1999 ), 625--653. Sturm, J. F. Using SeDuMi 1.02, a MATLAB toolbox for optimization over symmetric cones. Optimization methods and software 11, 1-4 (1999), 625--653."}],"event":{"name":"CPS-IoT Week '21: Cyber-Physical Systems and Internet of Things Week 2021","sponsor":["SIGBED ACM Special Interest Group on Embedded Systems","IEEE Signal Processing Society","IEEE CS"],"location":"Nashville Tennessee","acronym":"CPS-IoT Week '21"},"container-title":["Proceedings of the Workshop on Computation-Aware Algorithmic Design for Cyber-Physical Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3457335.3461715","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3457335.3461715","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3457335.3461715","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:17:19Z","timestamp":1750191439000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3457335.3461715"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,5,19]]},"references-count":9,"alternative-id":["10.1145\/3457335.3461715","10.1145\/3457335"],"URL":"https:\/\/doi.org\/10.1145\/3457335.3461715","relation":{},"subject":[],"published":{"date-parts":[[2021,5,19]]},"assertion":[{"value":"2021-06-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}