{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T09:25:20Z","timestamp":1750843520947,"version":"3.41.0"},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662482872"},{"type":"electronic","value":"9783662482889"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-662-48288-9_18","type":"book-chapter","created":{"date-parts":[[2015,9,1]],"date-time":"2015-09-01T02:26:24Z","timestamp":1441074384000},"page":"312-331","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration"],"prefix":"10.1007","author":[{"given":"Dario","family":"Cattaruzza","sequence":"first","affiliation":[]},{"given":"Alessandro","family":"Abate","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Schrammel","sequence":"additional","affiliation":[]},{"given":"Daniel","family":"Kroening","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,9,2]]},"reference":[{"issue":"7","key":"18_CR1","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/s00236-006-0035-7","volume":"43","author":"E Asarin","year":"2007","unstructured":"Asarin, E., Dang, T., Girard, A.: Hybridization methods for the analysis of nonlinear systems. Acta Informatica 43(7), 451\u2013476 (2007)","journal-title":"Acta Informatica"},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: PLDI, pp. 196\u2013207. ACM (2003)","DOI":"10.1145\/780822.781153"},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/3-540-46430-1_10","volume-title":"Hybrid Systems: Computation and Control","author":"O Botchkarev","year":"2000","unstructured":"Botchkarev, O., Tripakis, S.: Verification of hybrid systems with linear differential inclusions using ellipsoidal approximations. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 73\u201388. Springer, Heidelberg (2000)"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"Cattaruzza, D., Abate, A., Schrammel, P., Kroening, D.: Unbounded-time analysis of guarded lti systems with inputs by abstract acceleration (extended version). Technical report, University of Oxford (2015). arxiv.org\/abs\/1506.05607","DOI":"10.1007\/978-3-662-48288-9_18"},{"key":"18_CR5","doi-asserted-by":"crossref","unstructured":"Chutinan, A., Krogh, B.H.: Computing polyhedral approximations to flow pipes for dynamic systems. In: CDC, pp. 2089\u20132094. IEEE Computer Society (1998)","DOI":"10.1109\/CDC.1998.758642"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Mover, S., Tonetta, S.: SMT-based verification of hybrid systems. In: AAAI Conference on Artificial Intelligence. AAAI Press (2012)","DOI":"10.1007\/s10703-012-0158-0"},{"key":"18_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-540-45069-6_39","volume-title":"Computer Aided Verification","author":"MA Col\u00f3n","year":"2003","unstructured":"Col\u00f3n, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Hunt Jr, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420\u2013432. Springer, Heidelberg (2003)"},{"key":"18_CR8","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"18_CR9","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL, pp. 84\u201397. ACM (1978)","DOI":"10.1145\/512760.512770"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-642-25318-8_6","volume-title":"Programming Languages and Systems","author":"T Dang","year":"2011","unstructured":"Dang, T., Gawlitza, T.M.: Template-based unbounded time verification of affine hybrid automata. In: Yang, H. (ed.) APLAS 2011. LNCS, vol. 7078, pp. 34\u201349. Springer, Heidelberg (2011)"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/978-3-642-40196-1_13","volume-title":"Quantitative Evaluation of Systems","author":"Y Deng","year":"2013","unstructured":"Deng, Y., Rajhans, A., Julius, A.A.: STRONG: A Trajectory-Based Verification Toolbox for Hybrid Systems. In: Joshi, K., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 165\u2013168. Springer, Heidelberg (2013)"},{"key":"18_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-540-88387-6_14","volume-title":"Automated Technology for Verification and Analysis","author":"A Eggers","year":"2008","unstructured":"Eggers, A., Fr\u00e4nzle, M., Herde, C.: SAT modulo ODE: a direct SAT approach to hybrid systems. In: Cha, S.S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 171\u2013185. Springer, Heidelberg (2008)"},{"key":"18_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-540-24743-2_22","volume-title":"Hybrid Systems: Computation and Control","author":"A Fehnker","year":"2004","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)"},{"issue":"3","key":"18_CR14","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/s10703-006-0031-0","volume":"30","author":"M Fr\u00e4nzle","year":"2007","unstructured":"Fr\u00e4nzle, M., Herde, C.: HySAT: an efficient proof engine for bounded model checking of hybrid systems. Formal Methods in System Design 30(3), 179\u2013198 (2007)","journal-title":"Formal Methods in System Design"},{"key":"18_CR15","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. 3414, pp. 258\u2013273. Springer, Heidelberg (2005)"},{"key":"18_CR16","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":"18_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/978-3-642-31365-3_23","volume-title":"Automated Reasoning","author":"EM Clarke","year":"2012","unstructured":"Clarke, E.M., Gao, S., Avigad, J.: $$\\delta $$-complete decision procedures for satisfiability\u00a0over\u00a0the reals. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 286\u2013300. Springer, Heidelberg (2012)"},{"key":"18_CR18","doi-asserted-by":"publisher","first-page":"379","DOI":"10.1006\/cviu.1998.0674","volume":"72","author":"PK Ghosh","year":"1998","unstructured":"Ghosh, P.K., Kumar, K.V.: Support function representation of convex bodies, its application in geometric computing, and some related representations. Comput. Vis. Image Underst. 72, 379\u2013403 (1998)","journal-title":"Comput. Vis. Image Underst."},{"key":"18_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-540-31954-2_19","volume-title":"Hybrid Systems: Computation and Control","author":"A Girard","year":"2005","unstructured":"Girard, A.: Reachability of uncertain linear systems using zonotopes. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 291\u2013305. Springer, Heidelberg (2005)"},{"key":"18_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/11730637_21","volume-title":"Hybrid Systems: Computation and Control","author":"A Girard","year":"2006","unstructured":"Girard, A., Le Guernic, C., Maler, O.: Efficient computation of reachable sets of linear time-invariant systems with inputs. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 257\u2013271. Springer, Heidelberg (2006)"},{"key":"18_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1007\/11823230_10","volume-title":"Static Analysis","author":"L Gonnord","year":"2006","unstructured":"Gonnord, L., Halbwachs, N.: Combining widening and acceleration in linear relation analysis. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 144\u2013160. Springer, Heidelberg (2006)"},{"issue":"Part B","key":"18_CR22","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/j.scico.2013.09.016","volume":"93","author":"L Gonnord","year":"2014","unstructured":"Gonnord, L., Schrammel, P.: Abstract acceleration in linear relation analysis. Sci. Comput. Program. 93(Part B), 125\u2013153 (2014)","journal-title":"Sci. Comput. Program."},{"key":"18_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"540","DOI":"10.1007\/978-3-642-02658-4_40","volume-title":"Computer Aided Verification","author":"C Le Guernic","year":"2009","unstructured":"Le Guernic, C., Girard, A.: Reachability analysis of hybrid systems using support functions. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 540\u2013554. Springer, Heidelberg (2009)"},{"key":"18_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-540-70545-1_18","volume-title":"Computer Aided Verification","author":"S Gulwani","year":"2008","unstructured":"Gulwani, S., Tiwari, A.: Constraint-based approach for analysis of hybrid systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 190\u2013203. Springer, Heidelberg (2008)"},{"key":"18_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-58485-4_43","volume-title":"Static Analysis","author":"N Halbwachs","year":"1994","unstructured":"Halbwachs, N., Raymond, P., Proy, Y.E.: Verification of linear hybrid systems by means of convex approximations. In: LeCharlier, B. (ed.) SAS 1994. LNCS, vol. 864, pp. 223\u2013237. Springer, Heidelberg (1994)"},{"issue":"1\u20132","key":"18_CR26","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"TA Henzinger","year":"1997","unstructured":"Henzinger, T.A., Ho, P.H., Wong-Toi, H.: HyTech: A model checker for hybrid systems. J. Softw. Tools Technol. Transfer 1(1\u20132), 110\u2013122 (1997)","journal-title":"J. Softw. Tools Technol. Transfer"},{"key":"18_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-642-04761-9_23","volume-title":"Automated Technology for Verification and Analysis","author":"JM Howe","year":"2009","unstructured":"Howe, J.M., King, A.: Logahedra: a new weakly relational domain. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 306\u2013320. Springer, Heidelberg (2009)"},{"key":"18_CR28","unstructured":"Jeannet, B.: Interproc analyzer for recursive programs with numerical variables (2010). http:\/\/pop-art.inrialpes.fr\/interproc\/interprocweb.cgi"},{"key":"18_CR29","doi-asserted-by":"crossref","unstructured":"Jeannet, B., Schrammel, P., Sankaranarayanan, S.: Abstract acceleration of general linear loops. In: POPL, pp. 529\u2013540. ACM (2014)","DOI":"10.1145\/2578855.2535843"},{"key":"18_CR30","unstructured":"Johnson, T.T., Mitra, S.: Passel: A verification tool for parameterized networks of hybrid automata (2012). https:\/\/publish.illinois.edu\/passel-tool\/"},{"key":"18_CR31","doi-asserted-by":"crossref","unstructured":"Le Guernic, C.: Reachability analysis of hybrid systems with linear continuous dynamics. Univerit\u00e9 Joseph Fourier (2009)","DOI":"10.1007\/978-3-642-02658-4_40"},{"key":"18_CR32","unstructured":"L\u00f6hner, R.: Einschlie\u00dfung der L\u00f6sung gew\u00f6hnlicher Anfangs- und Randwertaufgaben und Anwendungen. Ph.D. thesis, Universit\u00e4t Karlsruhe (1988)"},{"key":"18_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"686","DOI":"10.1007\/978-3-642-22110-1_56","volume-title":"Computer Aided Verification","author":"S Sankaranarayanan","year":"2011","unstructured":"Sankaranarayanan, S., Tiwari, A.: Relational abstractions for continuous and hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 686\u2013702. Springer, Heidelberg (2011)"},{"key":"18_CR34","doi-asserted-by":"crossref","unstructured":"Schrammel, P., Jeannet, B.: Extending abstract acceleration to data-flow programs with numerical inputs. In: Numerical and Symbolic Abstract Domains. ENTCS, vol. 267, pp. 101\u2013114. Elsevier (2010)","DOI":"10.1016\/j.entcs.2010.09.009"},{"issue":"12","key":"18_CR35","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1016\/j.jsc.2011.12.051","volume":"47","author":"P Schrammel","year":"2012","unstructured":"Schrammel, P., Jeannet, B.: Applying abstract acceleration to (co-)reachability analysis of reactive programs. J. Symbolic Comput. 47(12), 1512\u20131532 (2012)","journal-title":"J. Symbolic Comput."},{"key":"18_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"482","DOI":"10.1007\/3-540-36580-X_35","volume-title":"Hybrid Systems: Computation and Control","author":"O Stursberg","year":"2003","unstructured":"Stursberg, O., Krogh, B.H.: Efficient representation and computation of reachable sets for hybrid systems. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 482\u2013497. Springer, Heidelberg (2003)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-48288-9_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T09:57:53Z","timestamp":1748599073000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-48288-9_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783662482872","9783662482889"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-48288-9_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"2 September 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}