{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,3]],"date-time":"2025-08-03T23:00:32Z","timestamp":1754262032425,"version":"3.28.0"},"reference-count":13,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010,3]]},"DOI":"10.1109\/date.2010.5457051","type":"proceedings-article","created":{"date-parts":[[2013,2,19]],"date-time":"2013-02-19T18:16:33Z","timestamp":1361297793000},"page":"1512-1517","source":"Crossref","is-referenced-by-count":10,"title":["BACH 2 : Bounded reachability checker for compositional linear hybrid systems"],"prefix":"10.1109","author":[{"family":"Lei Bu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"family":"You Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"family":"Linzhang Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"family":"Xin Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"family":"Xuandong Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","first-page":"299","article-title":"The MathSAT 4 SMT Solver","author":"bruttomesso","year":"0","journal-title":"Proc Int Conf Computer Aided Verification"},{"journal-title":"The Yices SMT Solver","year":"2006","author":"dutertre","key":"ref11"},{"key":"ref12","first-page":"298","author":"barrett","year":"2007","journal-title":"Proceedings of International Conference on Computer Aided Verification 07 LNCS 4590"},{"key":"ref13","article-title":"The Barcelogic SMT Solver","author":"bofill","year":"2008","journal-title":"Proceedings of International Conference on Computer Aided Verification 08 LNCS 5123"},{"key":"ref4","doi-asserted-by":"crossref","first-page":"209","DOI":"10.3233\/SAT190012","article-title":"Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure","volume":"1","author":"fr\u00e4nzle","year":"2007","journal-title":"Journal on Satisfiability Boolean Modeling and Computation"},{"key":"ref3","first-page":"118","article-title":"Bounded Model Checking","volume":"58","author":"biere","year":"2003","journal-title":"Advance in Computers"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2008.ECP.13"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.12.022"},{"key":"ref8","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/s100090050008","article-title":"HYTECH: a model checker for hybrid systems","volume":"1","author":"henzinger","year":"1997","journal-title":"Software Tools for Technology Transfer"},{"journal-title":"Path-Oriented Bounded Reachability Analysis of Compositional Linear Hybrid Systems","year":"2008","author":"bu","key":"ref7"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561342"},{"key":"ref9","first-page":"258","article-title":"PHAVer: Algorithmic Verification of Hybrid Systems past HyTech","author":"frehse","year":"0","journal-title":"Proceedings of International Conference on Hybrid Systems Computation and Control‘05 LNCS 2289"}],"event":{"name":"2010 Design, Automation & Test in Europe Conference & Exhibition (DATE 2010)","start":{"date-parts":[[2010,3,8]]},"location":"Dresden","end":{"date-parts":[[2010,3,12]]}},"container-title":["2010 Design, Automation & Test in Europe Conference & Exhibition (DATE 2010)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/5450668\/5456897\/05457051.pdf?arnumber=5457051","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,22]],"date-time":"2020-07-22T14:04:56Z","timestamp":1595426696000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/5457051\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,3]]},"references-count":13,"URL":"https:\/\/doi.org\/10.1109\/date.2010.5457051","relation":{},"subject":[],"published":{"date-parts":[[2010,3]]}}}