{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,21]],"date-time":"2026-07-21T23:03:59Z","timestamp":1784675039434,"version":"3.55.0"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2014,5,16]],"date-time":"2014-05-16T00:00:00Z","timestamp":1400198400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2014,8]]},"DOI":"10.1007\/s10703-014-0210-3","type":"journal-article","created":{"date-parts":[[2014,5,15]],"date-time":"2014-05-15T18:59:43Z","timestamp":1400180383000},"page":"42-62","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["SAT\u2013LP\u2013IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata"],"prefix":"10.1007","volume":"45","author":[{"given":"Dingbao","family":"Xie","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lei","family":"Bu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jianhua","family":"Zhao","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xuandong","family":"Li","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2014,5,16]]},"reference":[{"key":"210_CR1","doi-asserted-by":"crossref","unstructured":"Henzinger TA (1996) The theory of hybrid automata. In: Proceedings of LICS 1996. IEEE Computer Society, pp 278\u2013292","DOI":"10.1109\/LICS.1996.561342"},{"key":"210_CR2","volume-title":"Model checking","author":"E Clarke","year":"1999","unstructured":"Clarke E, Grumberg O, Peled D (1999) Model checking. MIT Press, Cambridge, MA"},{"key":"210_CR3","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Kopke PW, Puri A, Varaiya P (1998) What\u2019s decidable about hybrid automata? J Comput Syst Sci 94\u2013124","DOI":"10.1006\/jcss.1998.1581"},{"key":"210_CR4","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Ho P, Wong-Toi H (1998) Algorithmic analysis of nonlinear hybrid systems. In: IEEE transactions on automatic control, pp 540\u2013554","DOI":"10.1109\/9.664156"},{"key":"210_CR5","doi-asserted-by":"crossref","unstructured":"Alur R, Courcoubetis C, Halbwachs N et al. (1995) The algorithmic analysis of hybrid systems. Theor Comput Sci 138(1):3\u201334","DOI":"10.1016\/0304-3975(94)00202-T"},{"key":"210_CR6","doi-asserted-by":"crossref","unstructured":"Frehse G (2005) PHAVer: algorithmic verification of hybrid systems past HyTech. In: Proceedings of HSCC\u201905, LNCS 2289, pp 258\u2013273","DOI":"10.1007\/978-3-540-31954-2_17"},{"key":"210_CR7","doi-asserted-by":"crossref","unstructured":"Frehse G, Guernic CL, Donz\u00e9 A et al. (2011) SpaceEx: scalable verification of hybrid systems. In: CAV, pp 379\u2013395","DOI":"10.1007\/978-3-642-22110-1_30"},{"key":"210_CR8","doi-asserted-by":"crossref","unstructured":"Biere A, Cimatti A, Clarke E, Strichman O, Zhu Y (2003) Bounded model checking. In: Advance in computers, vol 58, Academic Press, London, pp 118\u2013149","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"210_CR9","unstructured":"Barrett CW, Sebastiani R, Seshia SA, Tinelli C (2009) Satisifiability modulo theories. In: Handbook of satisfiability, pp 825\u2013885"},{"key":"210_CR10","doi-asserted-by":"crossref","unstructured":"Audemard G, Bozzano M, Cimatti A et al. (2005) Verifying industrial hybrid systems with MathSAT. In: Proceedings of BMC2004, ENTCS, vol 119, Issue 2, Elsevier Science, pp 17\u201332","DOI":"10.1016\/j.entcs.2004.12.022"},{"key":"210_CR11","doi-asserted-by":"crossref","unstructured":"de Moura L, Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: Tools and algorithms for the construction and analysis of systems (TACAS), LNCS, vol 4963, pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"210_CR12","doi-asserted-by":"crossref","unstructured":"Li X, Jha S, Bu L (2007) Towards an efficient path-oriented tool for bounded reachability analysis of linear hybrid systems using linear programming. In: Proceedings of BMC06, ENTCS, vol 174, Issue 3, Elsevier Science, pp 57\u201370","DOI":"10.1016\/j.entcs.2006.12.023"},{"key":"210_CR13","doi-asserted-by":"crossref","unstructured":"Bu L, Li X (2011) Path-oriented bounded reachability analysis of composed linear hybrid systems. Softw Tools Technol Transf, 13(4):307\u2013317","DOI":"10.1007\/s10009-010-0163-9"},{"key":"210_CR14","doi-asserted-by":"crossref","unstructured":"Bu L, Li Y, Wang L, Li X (2008) BACH: bounded reachability checker for linear hybrid automata. In: FMCAD\u201908. IEEE Computer Society, pp 65\u201368","DOI":"10.1109\/FMCAD.2008.ECP.13"},{"key":"210_CR15","doi-asserted-by":"crossref","unstructured":"Biere A, Clarke E, Zhu Y (1999) Symbolic model checking without BDDs. In: TACAS\u201999, LNCS 1579. Springer, Berlin","DOI":"10.1007\/3-540-49059-0_14"},{"key":"210_CR16","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1287\/ijoc.3.2.157","volume":"3","author":"J Chinneck","year":"1991","unstructured":"Chinneck J, Dravnieks E (1991) Locating minimal infeasible constraint sets in linear programs. ORSA J Comput 3:157\u2013168","journal-title":"ORSA J Comput"},{"key":"210_CR17","unstructured":"E\u00e9 n N, S\u00f6rensson N (2004) An extensible SAT-solver. In: Theory and applications of satisfiability testing, vol 2919, pp 502\u2013518"},{"key":"210_CR18","unstructured":"CPLEX. http:\/\/www-01.ibm.com\/software\/integration\/optimization\/cplex-optimizer\/"},{"key":"210_CR19","unstructured":"SAT4J. http:\/\/www.sat4j.org\/"},{"key":"210_CR20","doi-asserted-by":"crossref","unstructured":"Jha S, Krogh BH, Weimer JE, Clarke EM (2007) Reachability for linear hybrid automata using iterative relaxation abstraction. In: Proceedings of HSCC\u201907, pp 287\u2013300","DOI":"10.1007\/978-3-540-71493-4_24"},{"key":"210_CR21","unstructured":"runlim. http:\/\/fmv.jku.at\/runlim\/"},{"key":"210_CR22","doi-asserted-by":"crossref","unstructured":"Cimatti A, Mover S, Tonetta S (2012) SMT-based verification of hybrid systems. In: AAAI","DOI":"10.1007\/s10703-012-0158-0"},{"key":"210_CR23","doi-asserted-by":"crossref","unstructured":"Cimatti A, Mover S, Tonetta S, (2013) SMT-based scenario verification for hybrid systems. Formal Methods Syst Des 42:46\u201366","DOI":"10.1007\/s10703-012-0158-0"},{"key":"210_CR24","doi-asserted-by":"crossref","unstructured":"Bruttomesso R et al. (2008) The MathSAT 4 SMT Solver. In: CAV, pp 299\u2013303","DOI":"10.1007\/978-3-540-70545-1_28"},{"key":"210_CR25","unstructured":"Audemard G et al. (2002) Bounded model checking for timed systems. In: Proceedings of conference on formal techniques for networked and distributed systems. In: LNCS 2529, pp 243\u2013259"},{"key":"210_CR26","doi-asserted-by":"crossref","unstructured":"Franzle M, Herde C (2007) HySAT: an efficient proof engine for bounded model checking of hybrid systems. Form Methods Syst Des 30(3):179\u2013198","DOI":"10.1007\/s10703-006-0031-0"},{"key":"210_CR27","doi-asserted-by":"crossref","unstructured":"\u00c1brah\u00e1m E, Becker B, Klaedtke F, Steffen M (2005) Optimizing bounded model checking for linear hybrid systems. In: Proceedings of VMCAI 2005, LNCS, vol 3385, pp 396\u2013412","DOI":"10.1007\/978-3-540-30579-8_26"},{"key":"210_CR28","doi-asserted-by":"crossref","unstructured":"Sheeran M, Singh S, Stalmarck G (2000) Checking safety properties using induction and a SAT solver. In: FMCAD, pp 108\u2013125","DOI":"10.1007\/3-540-40922-X_8"},{"key":"210_CR29","doi-asserted-by":"crossref","unstructured":"Jha S, Brady BA, Seshia SA (2007) Seshia symbolic reachability analysis of lazy linear hybrid automata. In: Formal modeling and analysis of timed systems, vol 4763. Springer, Berlin, pp 241\u2013256","DOI":"10.1007\/978-3-540-75454-1_18"},{"key":"210_CR30","doi-asserted-by":"crossref","unstructured":"Clarke E et al (2000) Counterexample-guided abstraction refinement. In: CAV 2000, LNCS 1855. Springer, Heidelberg, pp 154\u2013169","DOI":"10.1007\/10722167_15"},{"key":"210_CR31","doi-asserted-by":"crossref","unstructured":"Fehnker A, Clarke E, Kumar Jha S, Krogh B (2005) Refining abstractions of hybrid systems using counterexample fragments. In: Proceedings of HSCC\u201905, pp 242\u2013257","DOI":"10.1007\/978-3-540-31954-2_16"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-014-0210-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-014-0210-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-014-0210-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,10]],"date-time":"2019-08-10T14:00:35Z","timestamp":1565445635000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-014-0210-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,5,16]]},"references-count":31,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,8]]}},"alternative-id":["210"],"URL":"https:\/\/doi.org\/10.1007\/s10703-014-0210-3","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,5,16]]}}}