{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:29:59Z","timestamp":1759638599600,"version":"3.28.0"},"reference-count":35,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013,9]]},"DOI":"10.1109\/emsoft.2013.6658592","type":"proceedings-article","created":{"date-parts":[[2013,11,21]],"date-time":"2013-11-21T10:52:14Z","timestamp":1385031134000},"page":"1-10","source":"Crossref","is-referenced-by-count":11,"title":["Time-aware relational abstractions for hybrid systems"],"prefix":"10.1109","author":[{"given":"Sergio","family":"Mover","sequence":"first","affiliation":[]},{"given":"Alessandro","family":"Cimatti","sequence":"additional","affiliation":[]},{"given":"Ashish","family":"Tiwari","sequence":"additional","affiliation":[]},{"given":"Stefano","family":"Tonetta","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"19","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561342"},{"key":"35","first-page":"343","article-title":"Timed relational abstractions for sampled data control systems","author":"zutshi","year":"2012","journal-title":"CAV"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1109\/87.974337"},{"key":"18","first-page":"379","article-title":"SpaceEx: Scalable verification of hybrid systems","author":"frehse","year":"2011","journal-title":"CAV"},{"key":"33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_56"},{"key":"15","first-page":"496","author":"de moura","year":"2004","journal-title":"CAV"},{"key":"34","first-page":"600","article-title":"Nonlinear systems: Approximating reach sets","author":"tiwari","year":"2004","journal-title":"HSCC"},{"key":"16","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1145\/261320.261324","article-title":"REDLOG computer algebra meets computer logic","volume":"31","author":"dolzmann","year":"1996","journal-title":"ACM Sigsam Bulletin"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1142\/S012905410300190X"},{"key":"14","first-page":"14","article-title":"Bounded model checking and induction: From refutation to verification","author":"de moura","year":"2003","journal-title":"CAV"},{"key":"11","first-page":"187","article-title":"A quantifier-free SMT encoding of non-linear hybrid automata","author":"cimatti","year":"2012","journal-title":"FMCAD"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0158-0"},{"key":"21","article-title":"Surprises about some elementary functions: Uniform linear approximations","author":"hilscher","year":"2000","journal-title":"Technical Report"},{"key":"20","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050008"},{"key":"22","first-page":"157","article-title":"Generalized property directed reachability","author":"hoder","year":"2012","journal-title":"SAT"},{"key":"23","first-page":"339","article-title":"Solving non-linear arithmetic","author":"jovanovic","year":"2012","journal-title":"IJCAR"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.2001.0472"},{"key":"25","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2007.909810"},{"key":"26","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9103-8"},{"key":"27","first-page":"477","article-title":"Safety verification of hybrid systems using barrier certificates","author":"prajna","year":"2004","journal-title":"HSCC"},{"key":"28","first-page":"686","article-title":"Relational abstractions for continuous and hybrid systems","author":"sankaranarayanan","year":"2011","journal-title":"CAV"},{"key":"29","first-page":"108","article-title":"Checking safety properties using induction and a SAT-solver","author":"sheeran","year":"2000","journal-title":"FMCAD"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1145\/1132357.1132363"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1145\/2038642.2038685"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1109\/SEAA.2011.49"},{"key":"1","first-page":"396","article-title":"Optimizing bounded model checking for linear hybrid systems","author":"a?braha?m","year":"2005","journal-title":"VMCAI"},{"key":"30","first-page":"2002","article-title":"Bounded model checking for timed automata","author":"sorea","year":"2002","journal-title":"Electronic Notes in Theoretical Computer Science"},{"journal-title":"The Calculus of Computation - Decision Procedures with Application to Verification","year":"2007","author":"bradley","key":"7"},{"key":"6","first-page":"193","article-title":"Symbolic model checking without BDDs","author":"biere","year":"1999","journal-title":"TACAS"},{"key":"32","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-007-0044-3"},{"key":"5","first-page":"825","article-title":"Satisfiability modulo theories","author":"barrett","year":"2009","journal-title":"Handbook of Satisfiability"},{"key":"31","doi-asserted-by":"publisher","DOI":"10.1145\/1993886.1993935"},{"key":"4","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.12.022"},{"key":"9","first-page":"277","article-title":"Software model checking via IC3","author":"cimatti","year":"2012","journal-title":"CAV"},{"key":"8","doi-asserted-by":"publisher","DOI":"10.1145\/968708.968710"}],"event":{"name":"2013 International \u00a0Conference on Embedded \u00a0Software (EMSOFT)","start":{"date-parts":[[2013,9,29]]},"location":"Montreal, QC, Canada","end":{"date-parts":[[2013,10,4]]}},"container-title":["2013 Proceedings of the International Conference on Embedded Software (EMSOFT)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6648479\/6658572\/06658592.pdf?arnumber=6658592","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,21]],"date-time":"2017-06-21T22:54:00Z","timestamp":1498085640000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6658592\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,9]]},"references-count":35,"URL":"https:\/\/doi.org\/10.1109\/emsoft.2013.6658592","relation":{},"subject":[],"published":{"date-parts":[[2013,9]]}}}