{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,7]],"date-time":"2025-11-07T13:23:54Z","timestamp":1762521834032,"version":"3.41.0"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319251400"},{"type":"electronic","value":"9783319251417"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-25141-7_2","type":"book-chapter","created":{"date-parts":[[2015,10,31]],"date-time":"2015-10-31T08:51:25Z","timestamp":1446281485000},"page":"8-24","source":"Crossref","is-referenced-by-count":24,"title":["Current Challenges in the Verification of Hybrid Systems"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Schupp","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Erika","family":"\u00c1brah\u00e1m","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xin","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ibtissem","family":"Ben Makhlouf","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Goran","family":"Frehse","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sriram","family":"Sankaranarayanan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Kowalewski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,1]]},"reference":[{"issue":"4","key":"2_CR1","doi-asserted-by":"publisher","first-page":"903","DOI":"10.1109\/TRO.2014.2312453","volume":"30","author":"M Althoff","year":"2014","unstructured":"Althoff, M., Dolan, J.M.: Online verification of automated road vehicles using reachability analysis. IEEE Trans. Robot. 30(4), 903\u2013918 (2014)","journal-title":"IEEE Trans. Robot."},{"key":"2_CR2","unstructured":"Althoff, M., Frehse, G.: Benchmarks of the workshop on applied verification of continuous and hybrid systems (ARCH) (2014). http:\/\/cps-vo.org\/group\/ARCH\/benchmarks"},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Ames, A.D., Sastry, S.: Characterization of Zeno behavior in hybrid systems using homological methods. In: Proceedings of ACC 2005, pp. 1160\u20131165. IEEE Computer Society Press (2005)","DOI":"10.1109\/ACC.2005.1470118"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"Bak, S., Bogomolov, S., Johnson, T.T.: HYST: a source transformation and translation tool for hybrid automaton models. In: Proceedings of HSCC 2015, pp. 128\u2013133. ACM (2015)","DOI":"10.1145\/2728606.2728630"},{"key":"2_CR5","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The satisfiability modulo theories library (SMT-LIB) (2010). http:\/\/www.SMT-LIB.org"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"575","DOI":"10.1007\/978-3-642-54862-8_48","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"DA Beek van","year":"2014","unstructured":"van Beek, D.A., Fokkink, W.J., Hendriks, D., Hofkamp, A., Markovski, J., van de Mortel-Fronczak, J.M., Reniers, M.A.: CIF 3: model-based engineering of supervisory controllers. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 575\u2013580. Springer, Heidelberg (2014)"},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"Ben Makhlouf, I., Diab, H., Kowalewski, S.: Safety verification of a controlled cooperative platoon under loss of communication using zonotopes. In: Proceedings of ADHS 2012, pp. 333\u2013338. IFAC-PapersOnLine (2012)","DOI":"10.3182\/20120606-3-NL-3011.00057"},{"key":"2_CR8","unstructured":"Benchmarks of continuous and hybrid systems. http:\/\/ths.rwth-aachen.de\/research\/hypro\/benchmarks-of-continuous-and-hybrid-systems\/"},{"key":"2_CR9","series-title":"Lecture Notes in Control and Information Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/11587392_1","volume-title":"Stochastic Hybrid Systems","author":"M Bujorianu","year":"2006","unstructured":"Bujorianu, M., Lygeros, J.: Toward a general theory of stochastic hybrid systems. In: Blom, H.A.P., Lygeros, J. (eds.) Stochastic Hybrid Systems. LNCIS, vol. 337, pp. 3\u201330. Springer, Heidelberg (2006)"},{"key":"2_CR10","unstructured":"Chen, X.: Reachability Analysis of Non-Linear Hybrid Systems Using Taylor Models. Ph.D. thesis, RWTH Aachen University, Germany (2015)"},{"key":"2_CR11","doi-asserted-by":"crossref","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Taylor model flowpipe construction for non-linear hybrid systems. In: Proceedings of RTSS 2012, pp. 183\u2013192. IEEE Computer Society Press (2012)","DOI":"10.1109\/RTSS.2012.70"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-642-39799-8_18","volume-title":"Computer Aided Verification","author":"X Chen","year":"2013","unstructured":"Chen, X., \u00c1brah\u00e1m, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258\u2013263. Springer, Heidelberg (2013)"},{"key":"2_CR13","doi-asserted-by":"crossref","unstructured":"Collins, P., Bresolin, D., Geretti, L., Villa, T.: Computing the evolution of hybrid systems using rigorous function calculus. In: Proceedings of ADHS 2012, pp. 284\u2013290. IFAC-PapersOnLine (2012)","DOI":"10.3182\/20120606-3-NL-3011.00063"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of SIGACT-SIGPLAN, pp. 84\u201396. ACM (1978)","DOI":"10.1145\/512760.512770"},{"key":"2_CR15","unstructured":"Eggers, A.: Direct Handling of Ordinary Differential Equations in Constraint-solving-based Analysis of Hybrid Systems. Ph.D. thesis, Universit\u00e4t Oldenburg, Germany (2014)"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Fehnker, A., Ivan\u010di\u0107, F.: Benchmarks for hybrid systems verification. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 326\u2013341. Springer, Heidelberg (2004)","DOI":"10.1007\/978-3-540-24743-2_22"},{"key":"2_CR17","first-page":"209","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. J. Satisf. Boolean Model. Comput. 1, 209\u2013236 (2007)","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Frehse, G., Kateja, R., Le Guernic, C.: Flowpipe approximation and clustering in space-time. In: Proceedings of HSCC 2013, pp. 203\u2013212. ACM (2013)","DOI":"10.1145\/2461328.2461361"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Frehse, G.: Reachability of hybrid systems in space-time. In: Proceedings of EMSOFT 2015. ACM (2015)","DOI":"10.1109\/EMSOFT.2015.7318258"},{"key":"2_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1007\/978-3-642-22110-1_30","volume-title":"Computer Aided Verification","author":"G Frehse","year":"2011","unstructured":"Frehse, G., Le Guernic, C., Donz\u00e9, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379\u2013395. Springer, Heidelberg (2011)"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1007\/978-3-319-21401-6_36","volume-title":"Automated Deduction - CADE-25","author":"N Fulton","year":"2015","unstructured":"Fulton, N., Mitsch, S., Quesel, J.D., V\u00f6lp, M., Platzer, A.: KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS, vol. 9195, pp. 527\u2013538. Springer, Heidelberg (2015)"},{"key":"2_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-642-38574-2_14","volume-title":"Automated Deduction \u2013 CADE-24","author":"S Gao","year":"2013","unstructured":"Gao, S., Kong, S., Clarke, E.M.: dReal: an SMT Solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 208\u2013214. Springer, Heidelberg (2013)"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Henzinger, T.: The theory of hybrid automata. In: Proceedings of LICS 1996, pp. 278\u2013292. IEEE Computer Society Press (1996)","DOI":"10.1109\/LICS.1996.561342"},{"issue":"1","key":"2_CR24","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1006\/jcss.1998.1581","volume":"57","author":"TA Henzinger","year":"1998","unstructured":"Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What\u2019s decidable about hybrid automata? J. Comput. Syst. Sci. 57(1), 94\u2013124 (1998)","journal-title":"J. Comput. Syst. Sci."},{"key":"2_CR25","unstructured":"HyCreate: a tool for overapproximating reachability of hybrid automata. http:\/\/stanleybak.com\/projects\/hycreate\/hycreate.html"},{"key":"2_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/978-3-662-46681-0_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Kong","year":"2015","unstructured":"Kong, S., Gao, S., Chen, W., Clarke, E.: dReach: $$\\delta $$ \u03b4 -reachability analysis for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 200\u2013205. Springer, Heidelberg (2015)"},{"key":"2_CR27","unstructured":"Le Guernic, C.: Reachability analysis of hybrid systems with linear continuous dynamics. Ph.D. thesis, Universit\u00e9 Joseph-Fourier-Grenoble I, France (2009)"},{"issue":"2","key":"2_CR28","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1016\/j.nahs.2009.03.002","volume":"4","author":"C Guernic Le","year":"2010","unstructured":"Le Guernic, C., Girard, A.: Reachability analysis of linear systems using support functions. Nonlinear Anal. Hybrid Syst. 4(2), 250\u2013262 (2010)","journal-title":"Nonlinear Anal. Hybrid Syst."},{"key":"2_CR29","unstructured":"Lygeros, J.: Lecture notes on hybrid systems. In: Notes for the ENSIETA 2004 Workshop (2004)"},{"key":"2_CR30","unstructured":"Maka, H., Frehse, G., Krogh, B.H.: Polyhedral domains and widening for verification of numerical programs. In: NSV-II: Second International Workshop on Numerical Software Verification (2009)"},{"key":"2_CR31","unstructured":"Nedialkov, N.S.: VNODE-LP - A validated solver for initial value problems in ordinary differential equations. Technical Report CAS-06-06-NN, Department of Computing and Software, McMaster University, Ontario (2006)"},{"key":"2_CR32","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-540-71070-7_15","volume-title":"Automated Reasoning","author":"A Platzer","year":"2008","unstructured":"Platzer, A., Quesel, J.-D.: KeYmaera: a hybrid theorem prover for hybrid systems (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 171\u2013178. Springer, Heidelberg (2008)"},{"issue":"2","key":"2_CR33","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/s10817-008-9103-8","volume":"41","author":"A Platzer","year":"2008","unstructured":"Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reason. 41(2), 143\u2013189 (2008)","journal-title":"J. Autom. Reason."},{"key":"2_CR34","unstructured":"ProHVer: Safety verification for probabilistic hybrid systems. http:\/\/depend.cs.uni-sb.de\/tools\/prohver\/"},{"issue":"10","key":"2_CR35","doi-asserted-by":"publisher","first-page":"2352","DOI":"10.1109\/TAC.2009.2028974","volume":"54","author":"N Ramdani","year":"2009","unstructured":"Ramdani, N., Meslem, N., Candau, Y.: A hybrid bounding method for computing an over-approximation for the reachable set of uncertain nonlinear systems. IEEE Trans. Autom. Control 54(10), 2352\u20132364 (2009)","journal-title":"IEEE Trans. Autom. Control"},{"key":"2_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/978-3-540-31954-2_37","volume-title":"Hybrid Systems: Computation and Control","author":"S Ratschan","year":"2005","unstructured":"Ratschan, S., She, Z.: Safety verification of hybrid systems by constraint propagation based abstraction refinement. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 573\u2013589. Springer, Heidelberg (2005)"},{"key":"2_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-642-39718-9_20","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2013","author":"Z Shao","year":"2013","unstructured":"Shao, Z., Liu, J.: Spatio-temporal hybrid automata for cyber-physical systems. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) ICTAC 2013. LNCS, vol. 8049, pp. 337\u2013354. Springer, Heidelberg (2013)"},{"key":"2_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/3-540-45352-0_5","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"J Sproston","year":"2000","unstructured":"Sproston, J.: Decidable model checking of probabilistic hybrid automata. In: Joseph, M. (ed.) FTRTFT 2000. LNCS, vol. 1926, p. 31. Springer, Heidelberg (2000)"}],"container-title":["Lecture Notes in Computer Science","Cyber Physical Systems. Design, Modeling, and Evaluation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-25141-7_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T07:45:56Z","timestamp":1748677556000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-25141-7_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319251400","9783319251417"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-25141-7_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}