{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T09:59:54Z","timestamp":1740131994777,"version":"3.37.3"},"reference-count":28,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"11","license":[{"start":{"date-parts":[[2018,11,1]],"date-time":"2018-11-01T00:00:00Z","timestamp":1541030400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2018,11,1]],"date-time":"2018-11-01T00:00:00Z","timestamp":1541030400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2018,11,1]],"date-time":"2018-11-01T00:00:00Z","timestamp":1541030400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/100000028","name":"Semiconductor Research Corporation","doi-asserted-by":"publisher","award":["2012-TJ-2267","2017-CT-2740"],"award-info":[{"award-number":["2012-TJ-2267","2017-CT-2740"]}],"id":[{"id":"10.13039\/100000028","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Comput.-Aided Des. Integr. Circuits Syst."],"published-print":{"date-parts":[[2018,11]]},"DOI":"10.1109\/tcad.2018.2857361","type":"journal-article","created":{"date-parts":[[2018,7,19]],"date-time":"2018-07-19T18:51:30Z","timestamp":1532026290000},"page":"2474-2484","source":"Crossref","is-referenced-by-count":3,"title":["Formal Feature Interpretation of Hybrid Systems"],"prefix":"10.1109","volume":"37","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4590-0665","authenticated-orcid":false,"given":"Antonio Anastasio","family":"Bruto da Costa","sequence":"first","affiliation":[{"name":"Department of Computer Science and Engineering, Indian Institute of Technology Kharagpur, Kharagpur, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Goran","family":"Frehse","sequence":"additional","affiliation":[{"name":"Verimag, Université Grenoble Alpes, Saint-Martind’Hères, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pallab","family":"Dasgupta","sequence":"additional","affiliation":[{"name":"Department of Computer Science and Engineering, Indian Institute of Technology Kharagpur, Kharagpur, India"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","first-page":"379","article-title":"SpaceEx: Scalable verification of hybrid systems","author":"frehse","year":"2011","journal-title":"Proc CAV"},{"key":"ref11","first-page":"1","article-title":"Some recent results in metric temporal logic","author":"ouaknine","year":"2008","journal-title":"Proc FORMATS"},{"key":"ref12","first-page":"92","article-title":"Robust satisfaction of temporal logic over real-valued signals","author":"donz\u00e9","year":"2010","journal-title":"Proc FORMATS"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9413-9"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2016.2525798"},{"key":"ref15","doi-asserted-by":"crossref","first-page":"208","DOI":"10.1007\/978-3-319-67531-2_13","article-title":"Telex: Passive STL learning using only positive examples","author":"jha","year":"2017","journal-title":"Runtime Verification"},{"key":"ref16","first-page":"167","article-title":"Breach, a toolbox for verification and parameter synthesis of hybrid systems","author":"donz\u00e9","year":"2010","journal-title":"Proc CAV"},{"key":"ref17","first-page":"254","article-title":"S-TaLiRo: A tool for temporal logic falsification for hybrid systems","author":"annapureddy","year":"2011","journal-title":"Proc TACAS"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/MDAT.2014.2361720"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2016.7797740"},{"key":"ref28","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1145\/2883817.2883825","article-title":"From simulation models to hybrid automata using urgency and relaxation","author":"minopoli","year":"2016","journal-title":"Proc HSCC"},{"year":"0","key":"ref4"},{"journal-title":"Benchmarks of continuous and hybrid systems","year":"2015","author":"abraham","key":"ref27"},{"key":"ref3","first-page":"21","article-title":"Verification of analog and mixed-signal circuits using hybrid system techniques","volume":"3312","author":"dang","year":"2004","journal-title":"Proc FMCAD"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/TENCON.2009.5396176"},{"year":"0","key":"ref5"},{"key":"ref8","first-page":"324","article-title":"Model checking of analog systems using an analog specification language","author":"steinhorst","year":"2008","journal-title":"Proc DATE"},{"key":"ref7","first-page":"152","article-title":"Monitoring temporal properties of continuous signals","volume":"3253","author":"maler","year":"2004","journal-title":"Proc FORMATS-FTRTFT'04"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2002.806655"},{"key":"ref9","first-page":"412","article-title":"STL model checking of continuous and hybrid systems","author":"roehm","year":"2016","journal-title":"Proc ATVA"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"ref20","first-page":"437","article-title":"ForFET: A formal feature evaluation tool for hybrid systems","author":"da costa","year":"2017","journal-title":"Proc ATVA"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-006-0035-7"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/VLSID.2017.2"},{"key":"ref24","first-page":"208","article-title":"DReal: An SMT solver for nonlinear theories over the reals","author":"gao","year":"2013","journal-title":"Proc Automated Deduction - CADE"},{"key":"ref23","first-page":"19","article-title":"Benchmark: DC-to-DC switched-mode power converters (buck converters, boost converters, and buck-boost converters)","volume":"34","author":"nguyen","year":"2015","journal-title":"Proceedings of ARC"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1109\/32.489079"},{"key":"ref25","first-page":"200","article-title":"dReach: \n$\\delta $\n-reachability analysis for hybrid systems","author":"kong","year":"2015","journal-title":"Proc TACAS"}],"container-title":["IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/43\/8496924\/08413134.pdf?arnumber=8413134","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,16]],"date-time":"2023-08-16T17:29:37Z","timestamp":1692206977000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/8413134\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,11]]},"references-count":28,"journal-issue":{"issue":"11"},"URL":"https:\/\/doi.org\/10.1109\/tcad.2018.2857361","relation":{},"ISSN":["0278-0070","1937-4151"],"issn-type":[{"type":"print","value":"0278-0070"},{"type":"electronic","value":"1937-4151"}],"subject":[],"published":{"date-parts":[[2018,11]]}}}