{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,1]],"date-time":"2024-09-01T05:04:37Z","timestamp":1725167077695},"reference-count":44,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"3","license":[{"start":{"date-parts":[[2017,3,1]],"date-time":"2017-03-01T00:00:00Z","timestamp":1488326400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"funder":[{"name":"National Key Basic Research Program of China","award":["2014CB340703"]},{"name":"Joint NSFC-ISF Research Program"},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003977","name":"Israel Science Foundation","doi-asserted-by":"publisher","award":["61561146394"],"id":[{"id":"10.13039\/501100003977","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61572249","61632015","91318301","61321491","61472179"],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Collaborative Innovation Center of Novel Software Technology and Industrialization"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Comput."],"published-print":{"date-parts":[[2017,3,1]]},"DOI":"10.1109\/tc.2016.2604308","type":"journal-article","created":{"date-parts":[[2016,8,30]],"date-time":"2016-08-30T18:52:54Z","timestamp":1472583174000},"page":"416-430","source":"Crossref","is-referenced-by-count":7,"title":["Deriving Unbounded Reachability Proof of Linear Hybrid Automata during Bounded Checking Procedure"],"prefix":"10.1109","volume":"66","author":[{"given":"Dingbao","family":"Xie","sequence":"first","affiliation":[]},{"given":"Wen","family":"Xiong","sequence":"additional","affiliation":[]},{"given":"Lei","family":"Bu","sequence":"additional","affiliation":[]},{"given":"Xuandong","family":"Li","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.21236\/ADA476791"},{"key":"ref38","first-page":"477","article-title":"Safety verification of hybrid systems using barrier certificates","author":"prajna","year":"0","journal-title":"Proc 7th Int Workshop Hybrid Syst Comput Control"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_2"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_6"},{"key":"ref31","year":"1995"},{"key":"ref30","year":"2009"},{"key":"ref37","first-page":"187","article-title":"A\n counterexample-guided approach to parameter synthesis for linear hybrid automata","author":"frehse","year":"0","journal-title":"Proc 11th Int Workshop Hybrid Syst Comput Control"},{"key":"ref36","first-page":"326","article-title":"Benchmarks for hybrid systems past HyTech","author":"fehnker","year":"0","journal-title":"Proc 7th Int Workshop Hybrid Syst Comput Control"},{"key":"ref35","author":"clarke","year":"1999","journal-title":"Model checking"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31954-2_16"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2008.ECP.13"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24310-3_17"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34188-5_7"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1287\/ijoc.3.2.157"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71493-4_24"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2003.1214874"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2014.22"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-014-0210-3"},{"key":"ref17","first-page":"359","article-title":"NuSMV 2: An opensource tool for symbolic\n model checking","author":"cimatti","year":"0","journal-title":"Proc 14th Int Conf Comput Aided Verification"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"ref19","author":"baier","year":"0","journal-title":"Principles of Model Checking"},{"key":"ref28","first-page":"1","article-title":"Interpolation and SAT-based model checking","author":"mcmillan","year":"0","journal-title":"Proc 19th Int Conf Comput Aided Verification"},{"key":"ref4","first-page":"258","article-title":"PHAVer: Algorithmic verification of hybrid systems past HyTech","author":"frehse","year":"0","journal-title":"Proc 8th Int Workshop Hybrid Syst Comput Control"},{"key":"ref27","year":"2006"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050008"},{"key":"ref6","first-page":"118","article-title":"Bounded model checking","volume":"58","author":"biere","year":"2003","journal-title":"Advance in Computers"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1016\/j.nahs.2009.03.002"},{"key":"ref5","first-page":"379","article-title":"SpaceEx: Scalable verification of hybrid\n systems","author":"frehse","year":"0","journal-title":"Proc 23rd Int Conf Comput Aided Verification"},{"key":"ref8","first-page":"337","article-title":"Z3: An efficient SMT solver","author":"de moura","year":"0","journal-title":"Proc Theory Practice Softw 14th Int Conf Tools Algorithms Construction Anal Syst"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.12.022"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1998.1581"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.12.023"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561342"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"ref22","first-page":"14","article-title":"Bounded model checking and induction: From refutation to verification","author":"de moura","year":"0","journal-title":"Proc 15th Int Conf Comput Aided Verification"},{"key":"ref21","first-page":"108","article-title":"Checking\n safety properties using induction and a SAT solver","author":"sheeran","year":"0","journal-title":"Proc 3rd Int Conf Formal Methods Comput -Aided Des"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44829-2_17"},{"key":"ref24","first-page":"433","article-title":"Abstraction and counterexample-guided construction of \n$\\omega$\n-automata for model checking of\n step-discrete linear hybrid models","author":"segelken","year":"0","journal-title":"Proc 19th Int Conf Comput Aided Verification"},{"key":"ref41","first-page":"71","article-title":"Interpolants\n as classifiers","author":"sharma","year":"0","journal-title":"Proc 24th Int Conf Comput Aided Verification"},{"key":"ref23","first-page":"70","article-title":"SAT-based model checking without unrolling","author":"bradley","year":"0","journal-title":"Proc Int Conf Verification Model Checking Abstract Interpretation"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"ref26","year":"2011"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_45"},{"key":"ref25","first-page":"248","article-title":"Efficient Büchi automata from LTL formulae","author":"somenzi","year":"0","journal-title":"Proc 12th Int Conf Comput Aided Verification"}],"container-title":["IEEE Transactions on Computers"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/12\/7847504\/07556340.pdf?arnumber=7556340","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T16:38:32Z","timestamp":1642005512000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7556340\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,3,1]]},"references-count":44,"journal-issue":{"issue":"3"},"URL":"https:\/\/doi.org\/10.1109\/tc.2016.2604308","relation":{},"ISSN":["0018-9340"],"issn-type":[{"value":"0018-9340","type":"print"}],"subject":[],"published":{"date-parts":[[2017,3,1]]}}}