{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T10:46:31Z","timestamp":1761648391555,"version":"3.28.0"},"reference-count":39,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016,9]]},"DOI":"10.1109\/cca.2016.7587948","type":"proceedings-article","created":{"date-parts":[[2016,10,20]],"date-time":"2016-10-20T20:50:06Z","timestamp":1476996606000},"page":"1024-1029","source":"Crossref","is-referenced-by-count":2,"title":["Tutorial: Software tools for hybrid systems verification, transformation, and synthesis: C2E2, HyST, and TuLiP"],"prefix":"10.1109","author":[{"given":"Parasara Sridhar","family":"Duggirala","sequence":"first","affiliation":[]},{"given":"Chuchu","family":"Fan","sequence":"additional","affiliation":[]},{"given":"Matthew","family":"Potok","sequence":"additional","affiliation":[]},{"given":"Bolun","family":"Qi","sequence":"additional","affiliation":[]},{"given":"Sayan","family":"Mitra","sequence":"additional","affiliation":[]},{"given":"Mahesh","family":"Viswanathan","sequence":"additional","affiliation":[]},{"given":"Stanley","family":"Bak","sequence":"additional","affiliation":[]},{"given":"Sergiy","family":"Bogomolov","sequence":"additional","affiliation":[]},{"given":"Taylor T.","family":"Johnson","sequence":"additional","affiliation":[]},{"given":"Luan Viet","family":"Nguyen","sequence":"additional","affiliation":[]},{"given":"Christian","family":"Schilling","sequence":"additional","affiliation":[]},{"given":"Andrew","family":"Sogokon","sequence":"additional","affiliation":[]},{"given":"Hoang-Dung","family":"Tran","sequence":"additional","affiliation":[]},{"given":"Weiming","family":"Xiang","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref39","article-title":"Large-scale linear systems from order-reduction (benchmark proposal)","author":"tran","year":"2016","journal-title":"Workshop on Applied Verification for Continuous and Hybrid Systems"},{"key":"ref38","article-title":"Non-linear continuous systems for safety verification (benchmark proposal)","author":"sogokon","year":"2016","journal-title":"Workshop on Applied Verification for Continuous and Hybrid Systems"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1016\/j.automatica.2007.01.019"},{"key":"ref32","article-title":"Order-Reduction Abstractions for Safety Verification of High-Dimensional Linear Systems","author":"tran","year":"2016","journal-title":"ArXiv e-prints"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1145\/2593458.2593471"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2015.26"},{"key":"ref37","article-title":"Benchmark: A nonlinear reachability analysis test set from numerical analysis","author":"tran","year":"2015","journal-title":"Workshop on Applied Verification for Continuous and Hybrid Systems"},{"key":"ref36","article-title":"Charge pump phase-locked loops and full wave rectifiers for reachability analysis (benchmark proposal)","author":"beg","year":"2016","journal-title":"Workshop on Applied Verification for Continuous and Hybrid Systems"},{"key":"ref35","article-title":"Benchmark: Dc-to-dc switched-mode power converters (buck converters, boost converters, and buck-boost converters)","author":"nguyen","year":"2014","journal-title":"Applied Verification for Continuous and Hybrid Systems Workshop (ARCH 2014)"},{"key":"ref34","doi-asserted-by":"crossref","first-page":"1183","DOI":"10.23919\/ACC.2004.1386733","article-title":"Reachability analysis of hybrid control systems using reduced-order models","volume":"2","author":"han","year":"2004","journal-title":"American Control Conference 2004 Proceedings of the 2004"},{"key":"ref10","article-title":"Benchmarks for model transformations and conformance checking","author":"jin","year":"2014","journal-title":"1st International Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH)"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_5"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30476-0_23"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1016\/j.conengprac.2004.03.015"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/5.871304"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-007-0044-3"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_56"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_14"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"ref19","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-22110-1_30","article-title":"SpaceEx: Scalable verification of hybrid systems","author":"frehse","year":"2011","journal-title":"Computer Aided Verification (CAV) ser LNCS"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1145\/1755952.1755956"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_37"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-006-0035-7"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06410-9_16"},{"key":"ref6","article-title":"A lyapunov approach to incremental stability properties","author":"angeli","year":"2000","journal-title":"IEEE Trans Automat Contr"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1145\/2883817.2883837"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1016\/S0005-1098(98)00019-3"},{"journal-title":"Computer Assisted Proofs in Dynamic Groups (CAPD)","year":"0","key":"ref8"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24953-7_32"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/EMSOFT.2013.6658604"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1145\/2562059.2562140"},{"key":"ref1","article-title":"Control design for hybrid systems with tulip: The temporal logic planning toolbox (tutorial paper)","author":"dathathri","year":"2016","journal-title":"Multi-conference on Systems and Control"},{"key":"ref20","first-page":"1","article-title":"Guided search for hybrid systems based on coarse-grained space abstractions","author":"bogomolov","year":"2015","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39176-7_8"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-13338-6_10"},{"key":"ref24","article-title":"Satisfiability modulo ODEs","author":"gao","year":"2013","journal-title":"International Conference on Formal Methods in Computer-Aided Design (FMCAD)"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_18"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/2728606.2728630"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_4"}],"event":{"name":"2016 IEEE Conference on Control Applications (CCA)","start":{"date-parts":[[2016,9,19]]},"location":"Buenos Aires, Argentina","end":{"date-parts":[[2016,9,22]]}},"container-title":["2016 IEEE Conference on Control Applications (CCA)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/7581720\/7587772\/07587948.pdf?arnumber=7587948","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,14]],"date-time":"2019-09-14T21:32:32Z","timestamp":1568496752000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7587948\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,9]]},"references-count":39,"URL":"https:\/\/doi.org\/10.1109\/cca.2016.7587948","relation":{},"subject":[],"published":{"date-parts":[[2016,9]]}}}