{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,10]],"date-time":"2025-04-10T21:10:04Z","timestamp":1744319404012,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642341878"},{"type":"electronic","value":"9783642341885"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-34188-5_7","type":"book-chapter","created":{"date-parts":[[2012,10,11]],"date-time":"2012-10-11T14:04:33Z","timestamp":1349964273000},"page":"35-49","source":"Crossref","is-referenced-by-count":4,"title":["IIS-Guided DFS for Efficient Bounded Reachability Analysis of Linear Hybrid Automata"],"prefix":"10.1007","author":[{"given":"Lei","family":"Bu","sequence":"first","affiliation":[]},{"given":"Yang","family":"Yang","sequence":"additional","affiliation":[]},{"given":"Xuandong","family":"Li","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A.: The theory of hybrid automata. In: Proceedings of LICS 1996, pp. 278\u2013292. IEEE Computer Society (1996)","DOI":"10.1109\/LICS.1996.561342"},{"key":"7_CR2","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1006\/jcss.1998.1581","volume":"57","author":"T.A. Henzinger","year":"1998","unstructured":"Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What\u2019s Decidable About Hybrid Automata? Journal of Computer and System Sciences\u00a057, 94\u2013124 (1998)","journal-title":"Journal of Computer and System Sciences"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: Algorithmic Analysis of Nonlinear Hybrid Systems. IEEE Transactions on Automatic Control, 540\u2013554 (1998)","DOI":"10.1109\/9.664156"},{"key":"7_CR4","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R. Alur","year":"1995","unstructured":"Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical Computer Science\u00a0138, 3\u201334 (1995)","journal-title":"Theoretical Computer Science"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Strichman, O., Zhu, Y.: Bounded Model Checking. In: Advance in Computers, vol.\u00a058, pp. 118\u2013149. Academic Press (2003)","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"7_CR6","doi-asserted-by":"crossref","first-page":"209","DOI":"10.3233\/SAT190012","volume":"1","author":"M. Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle, M., Herde, C., Ratschan, S., Schubert, T., Teige, T.: Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. Journal on Satisfiability, Boolean Modeling and Computation\u00a01, 209\u2013236 (2007)","journal-title":"Journal on Satisfiability, Boolean Modeling and Computation"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Audemard, G., Bozzano, M., Cimatti, A., Sebastiani, R.: Verifying Industrial Hybrid Systems with MathSAT. In: Proceedings of BMC 2004, ENTCS, vol.\u00a0119(2), pp. 17\u201332. Elsevier Science (2005)","DOI":"10.1016\/j.entcs.2004.12.022"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Li, X., Jha, S.K., Bu, L.: Towards an Efficient Path-Oriented Tool for Bounded Reachability Analysis of Linear Hybrid Systems using Linear Programming. In: Proceedings of BMC 2006, ENTCS, vol.\u00a0174(3), pp. 57\u201370. Elsevier Science, 07 (2006)","DOI":"10.1016\/j.entcs.2006.12.023"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Bu, L., Li, Y., Wang, L., Li, X.: BACH: Bounded Reachability Checker for Linear Hybrid Automata. In: Proceedings of the 8th International Conference on Formal Methods in Computer Aided Design, pp. 65\u201368. IEEE Computer Society (2008)","DOI":"10.1109\/FMCAD.2008.ECP.13"},{"key":"7_CR10","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"T.A. Henzinger","year":"1997","unstructured":"Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: HYTECH: a model checker for hybrid systems. Software Tools for Technology Transfer\u00a01, 110\u2013122 (1997)","journal-title":"Software Tools for Technology Transfer"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-540-31954-2_17","volume-title":"Hybrid Systems: Computation and Control","author":"G. Frehse","year":"2005","unstructured":"Frehse, G.: PHAVer: Algorithmic Verification of Hybrid Systems Past HyTech. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol.\u00a03414, pp. 258\u2013273. Springer, Heidelberg (2005)"},{"key":"7_CR12","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1287\/ijoc.3.2.157","volume":"3","author":"J. Chinneck","year":"1991","unstructured":"Chinneck, J., Dravnieks, E.: Locating minimal infeasible constraint sets in linear programs. ORSA Journal on Computing\u00a03, 157\u2013168 (1991)","journal-title":"ORSA Journal on Computing"},{"issue":"4","key":"7_CR13","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/s10009-010-0163-9","volume":"13","author":"L. Bu","year":"2011","unstructured":"Bu, L., Li, X.: Path-Oriented Bounded Reachability Analysis of Composed Linear Hybrid Systems. Software Tools Technology Transfer\u00a013(4), 307\u2013317 (2011)","journal-title":"Software Tools Technology Transfer"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Bu, L., Li, Y., Wang, L., Chen, X., Li, X.: BACH 2: Bounded ReachAbility CHecker for Compositional Linear Hybrid Systems. In: Proceedings of the 13th Design Automation & Test in Europe Conference, Dresden, Germany, pp. 1512\u20131517 (2010)","DOI":"10.1109\/DATE.2010.5457051"},{"key":"7_CR15","unstructured":"OR-Objects, http:\/\/OpsResearch.com\/OR-Objects\/index.html"},{"issue":"1","key":"7_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0305-0548(94)90057-4","volume":"21","author":"J. Chinneck","year":"1994","unstructured":"Chinneck, J.: MINOS(IIS): Infeasibility analysis using MINOS. Computers and Operations Research\u00a021(1), 1\u20139 (1994)","journal-title":"Computers and Operations Research"},{"key":"7_CR17","unstructured":"CPLEX, http:\/\/www-01.ibm.com\/software\/integration\/optimization\/cplex-optimizer\/"},{"key":"7_CR18","unstructured":"L. Systems Inc., http:\/\/www.lindo.com\/products\/api\/dllm.html"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-540-71493-4_24","volume-title":"Hybrid Systems: Computation and Control","author":"S. Jha","year":"2007","unstructured":"Jha, S., Krogh, B.H., Weimer, J.E., Clarke, E.M.: Reachability for Linear Hybrid Automata Using Iterative Relaxation Abstraction. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol.\u00a04416, pp. 287\u2013300. Springer, Heidelberg (2007)"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software: Verification and Testing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-34188-5_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,10]],"date-time":"2025-04-10T20:52:07Z","timestamp":1744318327000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-34188-5_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642341878","9783642341885"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-34188-5_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}