{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T05:48:31Z","timestamp":1743054511798,"version":"3.40.3"},"publisher-location":"Cham","reference-count":52,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031223365"},{"type":"electronic","value":"9783031223372"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"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":[[2022]]},"DOI":"10.1007\/978-3-031-22337-2_3","type":"book-chapter","created":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T10:08:41Z","timestamp":1672222121000},"page":"39-60","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Symbolic Analysis of\u00a0Linear Hybrid Automata \u2013 25 Years Later"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5441-0481","authenticated-orcid":false,"given":"Goran","family":"Frehse","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8180-0904","authenticated-orcid":false,"given":"Mirco","family":"Giacobbe","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6388-2053","authenticated-orcid":false,"given":"Enea","family":"Zaffanella","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,12,29]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R.: Formal verification of hybrid systems. In: Chakraborty, S., Jerraya, A., Baruah, S.K., Fischmeister, S. (eds.) EMSOFT, pp. 273\u2013278. ACM (2011)","DOI":"10.1145\/2038642.2038685"},{"issue":"1","key":"3_CR2","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., et al.: The algorithmic analysis of hybrid systems. Theor. Comput. Sci. 138(1), 3\u201334 (1995)","journal-title":"Theor. Comput. Sci."},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/978-3-319-91908-9_22","volume-title":"Computing and Software Science","author":"R Alur","year":"2019","unstructured":"Alur, R., Giacobbe, M., Henzinger, T.A., Larsen, K.G., Miku\u010dionis, M.: Continuous-time models for system design and analysis. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 452\u2013477. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-319-91908-9_22"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Bacci, E., Giacobbe, M., Parker, D.: Verifying reinforcement learning up to infinity. In: IJCAI, pp. 2154\u20132160. ijcai.org (2021)","DOI":"10.24963\/ijcai.2021\/297"},{"issue":"2","key":"3_CR5","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/s00165-005-0061-1","volume":"17","author":"R Bagnara","year":"2005","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: Not necessarily closed convex polyhedra and the double description method. Formal Aspects Comput. 17(2), 222\u2013257 (2005)","journal-title":"Formal Aspects Comput."},{"issue":"1\u20132","key":"3_CR6","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2007.08.001","volume":"72","author":"R Bagnara","year":"2008","unstructured":"Bagnara, R., Hill, P.M., Zaffanella, E.: The parma polyhedra library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1\u20132), 3\u201321 (2008)","journal-title":"Sci. Comput. Program."},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-319-96145-3_13","volume-title":"Computer Aided Verification","author":"A Becchi","year":"2018","unstructured":"Becchi, A., Zaffanella, E.: A direct encoding for NNC polyhedra. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018, Part I. LNCS, vol. 10981, pp. 230\u2013248. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_13"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-319-99725-4_11","volume-title":"Static Analysis","author":"A Becchi","year":"2018","unstructured":"Becchi, A., Zaffanella, E.: An efficient abstract domain for not necessarily closed polyhedra. In: Podelski, A. (ed.) SAS 2018. LNCS, vol. 11002, pp. 146\u2013165. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-99725-4_11"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-030-32304-2_10","volume-title":"Static Analysis","author":"A Becchi","year":"2019","unstructured":"Becchi, A., Zaffanella, E.: Revisiting polyhedral analysis for hybrid systems. In: Chang, B.-Y.E. (ed.) SAS 2019. LNCS, vol. 11822, pp. 183\u2013202. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-32304-2_10"},{"key":"3_CR10","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2020.104620","volume":"275","author":"A Becchi","year":"2020","unstructured":"Becchi, A., Zaffanella, E.: PPLite: zero-overhead encoding of NNC polyhedra. Inf. Comput. 275, 104620 (2020)","journal-title":"Inf. Comput."},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/978-3-662-54577-5_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Bogomolov","year":"2017","unstructured":"Bogomolov, S., Frehse, G., Giacobbe, M., Henzinger, T.A.: Counterexample-guided refinement of template polyhedra. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 589\u2013606. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_34"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Boulm\u00e9, S., Mar\u00e9chal, A., Monniaux, D., P\u00e9rin, M., Yu, H.: The verified polyhedron library: an overview. In: 20th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2018, Timisoara, Romania, 20\u201323 September 2018, pp. 9\u201317. IEEE (2018)","DOI":"10.1109\/SYNASC.2018.00014"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Bu, L., et al.: ARCH-COMP20 category report: hybrid systems with piecewise constant dynamics and bounded model checking. In: ARCH20. 7th International Workshop on Applied Verification of Continuous and Hybrid Systems (ARCH20), Berlin, Germany, 12 July 2020. EPiC Series in Computing, vol. 74, pp. 1\u201315. EasyChair (2020)","DOI":"10.29007\/bhwx"},{"key":"3_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: Design, Automation and Test in Europe, DATE 2010, Dresden, Germany, 8\u201312 March 2010, pp. 1512\u20131517 (2010)","DOI":"10.1109\/DATE.2010.5457051"},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"535","DOI":"10.1007\/978-3-642-27549-4_69","volume-title":"Computer Aided Systems Theory \u2013 EUROCAST 2011","author":"X Chen","year":"2012","unstructured":"Chen, X., \u00c1brah\u00e1m, E.: Choice of directions for the approximation of reachable sets for hybrid systems. In: Moreno-D\u00edaz, R., Pichler, F., Quesada-Arencibia, A. (eds.) EUROCAST 2011. LNCS, vol. 6927, pp. 535\u2013542. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-27549-4_69"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Chernikova, N.V.: Algorithm for discovering the set of all solutions of a linear programming problem. U.S.S.R. Computational Mathematics and Mathematical Physics 8(6), 282\u2013293 (1968)","DOI":"10.1016\/0041-5553(68)90115-8"},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/10722167_15","volume-title":"Computer Aided Verification","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154\u2013169. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/10722167_15"},{"key":"3_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"EM Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52\u201371. Springer, Heidelberg (1982). https:\/\/doi.org\/10.1007\/BFb0025774"},{"key":"3_CR19","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: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL 1977, New York, NY, USA, pp. 238\u2013252. Association for Computing Machinery (1977)","DOI":"10.1145\/512950.512973"},{"key":"3_CR20","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Aho, A.V., Zilles, S.N., Szymanski, T.G. (eds.) Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, Tucson, Arizona, USA, January 1978, pp. 84\u201396. ACM Press (1978)","DOI":"10.1145\/512760.512770"},{"key":"3_CR21","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). https:\/\/doi.org\/10.1007\/978-3-642-25318-8_6"},{"issue":"3","key":"3_CR22","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s10009-007-0062-x","volume":"10","author":"G Frehse","year":"2008","unstructured":"Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. STTT 10(3), 263\u2013279 (2008)","journal-title":"STTT"},{"key":"3_CR23","unstructured":"Frehse, G., et al.: ARCH-COMP19 category report: hybrid systems with piecewise constant dynamics. In: Frehse, G., Althoff, M. (eds.) ARCH19 6th International Workshop on Applied Verification of Continuous and Hybrid Systems. EPiC Series in Computing, vol. 61, pp. 1\u201313. EasyChair (2019)"},{"key":"3_CR24","doi-asserted-by":"crossref","unstructured":"Frehse, G., et al.: ARCH-COMP18 category report: hybrid systems with piecewise constant dynamics. In: Frehse, G. (eds.) ARCH18 5th International Workshop on Applied Verification of Continuous and Hybrid Systems. EPiC Series in Computing, vol. 54, pp. 1\u201313. EasyChair (2018)","DOI":"10.29007\/p11g"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Frehse, G., Bogomolov, S., Greitschus, M., Strump, T., Podelski, A.: Eliminating spurious transitions in reachability with support functions. In: Girard, A., Sankaranarayanan, S. (eds.) Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, HSCC 2015, Seattle, WA, USA, 14\u201316 April 2015, pp. 149\u2013158. ACM (2015)","DOI":"10.1145\/2728606.2728622"},{"key":"3_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"468","DOI":"10.1007\/978-3-319-96145-3_25","volume-title":"Computer Aided Verification","author":"G Frehse","year":"2018","unstructured":"Frehse, G., Giacobbe, M., Henzinger, T.A.: Space-time interpolants. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 468\u2013486. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_25"},{"key":"3_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-540-78929-1_14","volume-title":"Hybrid Systems: Computation and Control","author":"G Frehse","year":"2008","unstructured":"Frehse, G., Jha, S.K., Krogh, B.H.: A counterexample-guided approach to parameter synthesis for linear hybrid automata. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 187\u2013200. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78929-1_14"},{"key":"3_CR28","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., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379\u2013395. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_30"},{"issue":"1","key":"3_CR29","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/s10703-006-0013-2","volume":"29","author":"N Halbwachs","year":"2006","unstructured":"Halbwachs, N., Merchat, D., Gonnord, L.: Some ways to reduce the space dimension in polyhedra computations. Formal Methods Syst. Des. 29(1), 79\u201395 (2006)","journal-title":"Formal Methods Syst. Des."},{"key":"3_CR30","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., Proy, Y.-E., Raymond, P.: Verification of linear hybrid systems by means of convex approximations. In: Le Charlier, B. (ed.) SAS 1994. LNCS, vol. 864, pp. 223\u2013237. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58485-4_43"},{"issue":"2","key":"3_CR31","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1023\/A:1008678014487","volume":"11","author":"N Halbwachs","year":"1997","unstructured":"Halbwachs, N., Proy, Y., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Formal Methods Syst. Des. 11(2), 157\u2013185 (1997)","journal-title":"Formal Methods Syst. Des."},{"key":"3_CR32","unstructured":"Henzinger, T.: The theory of hybrid automata. In: Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, pp. 278 (1996)"},{"key":"3_CR33","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"T Henzinger","year":"1997","unstructured":"Henzinger, T., Ho, P.-H., Wong-Toi, H.: HyTech: a model checker for hybrid systems. Softw. Tools Technol. Transf. 1, 110\u2013122 (1997)","journal-title":"Softw. Tools Technol. Transf."},{"key":"3_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/3-540-60472-3_14","volume-title":"Hybrid Systems II","author":"TA Henzinger","year":"1995","unstructured":"Henzinger, T.A., Ho, P.-H.: HyTech: the Cornell hybrid technology tool. In: Antsaklis, P., Kohn, W., Nerode, A., Sastry, S. (eds.) HS 1994. LNCS, vol. 999, pp. 265\u2013293. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60472-3_14"},{"key":"3_CR35","doi-asserted-by":"publisher","first-page":"540","DOI":"10.1109\/9.664156","volume":"43","author":"TA Henzinger","year":"1998","unstructured":"Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: Algorithmic analysis of nonlinear hybrid systems. IEEE Trans. Autom. Control 43, 540\u2013554 (1998)","journal-title":"IEEE Trans. Autom. Control"},{"key":"3_CR36","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, 94\u2013124 (1998)","journal-title":"J. Comput. Syst. Sci."},{"key":"3_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"661","DOI":"10.1007\/978-3-642-02658-4_52","volume-title":"Computer Aided Verification","author":"B Jeannet","year":"2009","unstructured":"Jeannet, B., Min\u00e9, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661\u2013667. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_52"},{"key":"3_CR38","doi-asserted-by":"crossref","unstructured":"Jha, S.K., Krogh, B.H., Weimer, J.E., Clarke, E.M.: Reachability for linear hybrid automata using iterative relaxation abstraction. In: HSCC, pp. 287\u2013300 (2007)","DOI":"10.1007\/978-3-540-71493-4_24"},{"key":"3_CR39","doi-asserted-by":"crossref","unstructured":"Le Guernic, C., Girard, A.: Reachability analysis of linear systems using support functions. Nonlinear Anal. Hybrid Syst. 4(2), 250\u2013262 (2010). IFAC World Congress 2008","DOI":"10.1016\/j.nahs.2009.03.002"},{"key":"3_CR40","doi-asserted-by":"crossref","unstructured":"Maler, O.: Algorithmic verification of continuous and hybrid systems. In: International Workshop on Verification of Infinite-State System (Infinity) (2013)","DOI":"10.4204\/EPTCS.140.4"},{"issue":"1","key":"3_CR41","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The octagon abstract domain. High. Order Symb. Comput. 19(1), 31\u2013100 (2006)","journal-title":"High. Order Symb. Comput."},{"key":"3_CR42","doi-asserted-by":"crossref","unstructured":"Motzkin, T.S., Raiffa, H., Thompson, G.L., Thrall, R.M.: The double description method. In: Kuhn, H.W., Tucker, A.W. (eds.) Contributions to the Theory of Games \u2013 Volume II, no. 28. Annals of Mathematics Studies, pp. 51\u201373. Princeton University Press, Princeton, New Jersey (1953)","DOI":"10.1515\/9781400881970-004"},{"key":"3_CR43","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: ARMC: the logical choice for software model checking with abstraction refinement. In: PADL, pp. 245\u2013259 (2007)","DOI":"10.1007\/978-3-540-69611-7_16"},{"key":"3_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"JP Queille","year":"1982","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337\u2013351. Springer, Heidelberg (1982). https:\/\/doi.org\/10.1007\/3-540-11494-7_22"},{"key":"3_CR45","unstructured":"Rockafellar, R.T. : Convex Analysis. Princeton University Press, Princeton (1970)"},{"key":"3_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1007\/978-3-662-49674-9_48","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N Roohi","year":"2016","unstructured":"Roohi, N., Prabhakar, P., Viswanathan, M.: Hybridization based CEGAR for hybrid automata with affine dynamics. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 752\u2013769. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_48"},{"key":"3_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/11609773_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S Sankaranarayanan","year":"2005","unstructured":"Sankaranarayanan, S., Col\u00f3n, M.A., Sipma, H., Manna, Z.: Efficient strongly relational polyhedral analysis. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 111\u2013125. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11609773_8"},{"key":"3_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-540-78800-3_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Sankaranarayanan","year":"2008","unstructured":"Sankaranarayanan, S., Dang, T., Ivan\u010di\u0107, F.: Symbolic model checking of hybrid systems using template polyhedra. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 188\u2013202. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_14"},{"key":"3_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-540-30579-8_2","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S Sankaranarayanan","year":"2005","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 25\u201341. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-30579-8_2"},{"key":"3_CR50","doi-asserted-by":"crossref","unstructured":"Singh, G., P\u00fcschel, M., Vechev, M.T.: Fast polyhedra abstract domain. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, 18\u201320 January 2017, pp. 46\u201359. ACM (2017)","DOI":"10.1145\/3009837.3009885"},{"key":"3_CR51","doi-asserted-by":"publisher","unstructured":"Tabuada, P.: Verification and Control of Hybrid Systems: A Symbolic Approach. Springer, New York (2009). https:\/\/doi.org\/10.1007\/978-1-4419-0224-5","DOI":"10.1007\/978-1-4419-0224-5"},{"issue":"9","key":"3_CR52","doi-asserted-by":"publisher","first-page":"681","DOI":"10.1080\/00029890.1986.11971923","volume":"93","author":"HP Williams","year":"1986","unstructured":"Williams, H.P.: Fourier\u2019s method of linear programming and its dual. Am. Math. Mon. 93(9), 681\u2013695 (1986)","journal-title":"Am. Math. Mon."}],"container-title":["Lecture Notes in Computer Science","Principles of Systems Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-22337-2_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,11]],"date-time":"2024-10-11T02:54:29Z","timestamp":1728615269000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-22337-2_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031223365","9783031223372"],"references-count":52,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-22337-2_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 December 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}