{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,30]],"date-time":"2026-05-30T04:44:01Z","timestamp":1780116241580,"version":"3.54.0"},"publisher-location":"New York, NY, USA","reference-count":48,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,4,16]],"date-time":"2019-04-16T00:00:00Z","timestamp":1555372800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Defense Advanced Research Projects Agency (DARPA)","award":["FA8750-18-C-0089"],"award-info":[{"award-number":["FA8750-18-C-0089"]}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation (NSF)","doi-asserted-by":"publisher","award":["CNS 1464311, CNS 1713253, SHF 1527398, SHF 1736323"],"award-info":[{"award-number":["CNS 1464311, CNS 1713253, SHF 1527398, SHF 1736323"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Air Force Office of Scientific Research (AFOSR)","award":["FA9550-15-1-0258, FA9550-16-1-0246, FA9550-18-1-0122, FA8650-12-3-7255"],"award-info":[{"award-number":["FA9550-15-1-0258, FA9550-16-1-0246, FA9550-18-1-0122, FA8650-12-3-7255"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,4,16]]},"DOI":"10.1145\/3302504.3311792","type":"proceedings-article","created":{"date-parts":[[2019,4,8]],"date-time":"2019-04-08T13:37:58Z","timestamp":1554730678000},"page":"23-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":25,"title":["Numerical verification of affine systems with up to a billion dimensions"],"prefix":"10.1145","author":[{"given":"Stanley","family":"Bak","sequence":"first","affiliation":[{"name":"Safe Sky Analytics"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hoang-Dung","family":"Tran","sequence":"additional","affiliation":[{"name":"Vanderbilt University"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Taylor T.","family":"Johnson","sequence":"additional","affiliation":[{"name":"Vanderbilt University"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,4,16]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Reachability Analysis of Large Linear Systems with Uncertain Inputs in the Krylov Subspace. arXiv preprint arXiv:1712.00369","author":"Althoff Matthias","year":"2017","unstructured":"Matthias Althoff . 2017. Reachability Analysis of Large Linear Systems with Uncertain Inputs in the Krylov Subspace. arXiv preprint arXiv:1712.00369 ( 2017 ). Matthias Althoff. 2017. Reachability Analysis of Large Linear Systems with Uncertain Inputs in the Krylov Subspace. arXiv preprint arXiv:1712.00369 (2017)."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2008.4738704"},{"key":"e_1_3_2_1_3_1","volume-title":"Hybrid systems","author":"Alur Rajeev","unstructured":"Rajeev Alur , Costas Courcoubetis , Thomas A Henzinger , and Pei-Hsin Ho. 1993. Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems . In Hybrid systems . Springer , 209--229. Rajeev Alur, Costas Courcoubetis, Thomas A Henzinger, and Pei-Hsin Ho. 1993. Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In Hybrid systems. Springer, 209--229."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/1987389.1987416"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1090\/conm\/280\/04630"},{"key":"e_1_3_2_1_6_1","volume-title":"The principle of minimized iterations in the solution of the matrix eigenvalue problem. Quarterly of applied mathematics 9, 1","author":"Arnoldi Walter Edwin","year":"1951","unstructured":"Walter Edwin Arnoldi . 1951. The principle of minimized iterations in the solution of the matrix eigenvalue problem. Quarterly of applied mathematics 9, 1 ( 1951 ). Walter Edwin Arnoldi. 1951. The principle of minimized iterations in the solution of the matrix eigenvalue problem. Quarterly of applied mathematics 9, 1 (1951)."},{"key":"e_1_3_2_1_7_1","volume-title":"5th International Workshop on Applied Verification of Continuous and Hybrid Systems (EPiC Series in Computing), Goran Frehse (Ed.)","volume":"54","author":"Bak Stanley","year":"2018","unstructured":"Stanley Bak . 2018 . Numerical Verification of 10000-dimensional Linear Systems 10000x Faster. In ARCH18 . 5th International Workshop on Applied Verification of Continuous and Hybrid Systems (EPiC Series in Computing), Goran Frehse (Ed.) , Vol. 54 . EasyChair, 135--144. Stanley Bak. 2018. Numerical Verification of 10000-dimensional Linear Systems 10000x Faster. In ARCH18. 5th International Workshop on Applied Verification of Continuous and Hybrid Systems (EPiC Series in Computing), Goran Frehse (Ed.), Vol. 54. EasyChair, 135--144."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2883817.2883837"},{"key":"e_1_3_2_1_9_1","volume-title":"4th International Workshop on Applied Verification of Continuous and Hybrid Systems (EPiC). Easy Chair.","author":"Bak Stanley","year":"2017","unstructured":"Stanley Bak and Parasara Sridhar Duggirala . 2017 . Direct Verification of Linear Systems with over 10000 Dimensions . In 4th International Workshop on Applied Verification of Continuous and Hybrid Systems (EPiC). Easy Chair. Stanley Bak and Parasara Sridhar Duggirala. 2017. Direct Verification of Linear Systems with over 10000 Dimensions. In 4th International Workshop on Applied Verification of Continuous and Hybrid Systems (EPiC). Easy Chair."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3049797.3049808"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63387-9_20"},{"key":"e_1_3_2_1_12_1","volume-title":"Hamilton-Jacobi Reachability: A Brief Overview and Recent Advances. 1709.07523","author":"Bansal Somil","year":"2017","unstructured":"Somil Bansal , Mo Chen , Sylvia Herbert , and Claire J Tomlin . 2017. Hamilton-Jacobi Reachability: A Brief Overview and Recent Advances. 1709.07523 ( 2017 ). Somil Bansal, Mo Chen, Sylvia Herbert, and Claire J Tomlin. 2017. Hamilton-Jacobi Reachability: A Brief Overview and Recent Advances. 1709.07523 (2017)."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3178126.3178128"},{"key":"e_1_3_2_1_14_1","unstructured":"Younes Chahlaoui and Paul Van Dooren. 2002. A collection of benchmark examples for model reduction of linear time invariant dynamical systems. (2002).  Younes Chahlaoui and Paul Van Dooren. 2002. A collection of benchmark examples for model reduction of linear time invariant dynamical systems. (2002)."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2012.70"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-17524-9_29"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Yi Chou Xin Chen and Sriram Sankaranarayanan. 2017. A Study of Model-Order Reduction Techniques for Verification. In Numerical Software Verification.  Yi Chou Xin Chen and Sriram Sankaranarayanan. 2017. A Study of Model-Order Reduction Techniques for Verification. In Numerical Software Verification.","DOI":"10.1007\/978-3-319-63501-9_8"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1755952.1755956"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_17"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_5"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"crossref","unstructured":"Parasara Sridhar Duggirala and Mahesh Viswanathan. 2016. Parsimonious simulation based verification of linear systems. In Computer Aided Verification.  Parasara Sridhar Duggirala and Mahesh Viswanathan. 2016. Parsimonious simulation based verification of linear systems. In Computer Aided Verification.","DOI":"10.1007\/978-3-319-41528-4_26"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"crossref","unstructured":"Chuchu Fan and Sayan Mitra. 2015. Bounded verification with on-the-fly discrepancy computation. In Automated Technology for Verification and Analysis.  Chuchu Fan and Sayan Mitra. 2015. Bounded verification with on-the-fly discrepancy computation. In Automated Technology for Verification and Analysis.","DOI":"10.1007\/978-3-319-24953-7_32"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_29"},{"key":"e_1_3_2_1_24_1","unstructured":"Stanley J Farlow. 1993. Partial differential equations for scientists and engineers.  Stanley J Farlow. 1993. Partial differential equations for scientists and engineers."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2461328.2461361"},{"key":"e_1_3_2_1_26_1","volume-title":"SpaceEx: Scalable Verification of Hybrid Systems. In International Conference on Computer Aided Verification. Springer.","author":"Frehse Goran","year":"2011","unstructured":"Goran Frehse , Colas Le Guernic , Alexandre Donz\u00e9 , Scott Cotton , Rajarshi Ray , Olivier Lebeltel , Rodolfo Ripado , Antoine Girard , Thao Dang , and Oded Maler . 2011 . SpaceEx: Scalable Verification of Hybrid Systems. In International Conference on Computer Aided Verification. Springer. Goran Frehse, Colas Le Guernic, Alexandre Donz\u00e9, Scott Cotton, Rajarshi Ray, Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, and Oded Maler. 2011. SpaceEx: Scalable Verification of Hybrid Systems. In International Conference on Computer Aided Verification. Springer."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1137\/0913071"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31954-2_19"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/11730637_21"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2007.895849"},{"key":"e_1_3_2_1_31_1","volume-title":"Approximate bisimulation: A bridge between computer science and control theory. European Journal of Control","author":"Girard Antoine","year":"2011","unstructured":"Antoine Girard and George J Pappas . 2011. Approximate bisimulation: A bridge between computer science and control theory. European Journal of Control ( 2011 ). Antoine Girard and George J Pappas. 2011. Approximate bisimulation: A bridge between computer science and control theory. European Journal of Control (2011)."},{"key":"e_1_3_2_1_32_1","volume-title":"An Efficient Algorithm for Vertex Enumeration of Two-Dimensional Projection of Polytopes. CoRR abs\/1611.10059","author":"Gurung Amit","year":"2016","unstructured":"Amit Gurung and Rajarshi Ray . 2016. An Efficient Algorithm for Vertex Enumeration of Two-Dimensional Projection of Polytopes. CoRR abs\/1611.10059 ( 2016 ). http:\/\/arxiv.org\/abs\/1611.10059 Amit Gurung and Rajarshi Ray. 2016. An Efficient Algorithm for Vertex Enumeration of Two-Dimensional Projection of Polytopes. CoRR abs\/1611.10059 (2016). http:\/\/arxiv.org\/abs\/1611.10059"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_27"},{"key":"e_1_3_2_1_35_1","volume-title":"American Control Conference.","author":"Han Zhi","year":"2004","unstructured":"Zhi Han and Bruce Krogh . 2004 . Reachability analysis of hybrid control systems using reduced-order models . In American Control Conference. Zhi Han and Bruce Krogh. 2004. Reachability analysis of hybrid control systems using reduced-order models. In American Control Conference."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/11730637_23"},{"key":"e_1_3_2_1_37_1","volume-title":"An iteration method for the solution of the eigenvalue problem of linear differential and integral operators","author":"Lanczos Cornelius","unstructured":"Cornelius Lanczos . 1950. An iteration method for the solution of the eigenvalue problem of linear differential and integral operators . USA Press Office . Cornelius Lanczos. 1950. An iteration method for the solution of the eigenvalue problem of linear differential and integral operators. USA Press Office."},{"key":"e_1_3_2_1_39_1","volume-title":"Reachability analysis of linear systems using support functions. Nonlinear Analysis: Hybrid Systems 4, 2","author":"Guernic Colas Le","year":"2010","unstructured":"Colas Le Guernic and Antoine Girard . 2010. Reachability analysis of linear systems using support functions. Nonlinear Analysis: Hybrid Systems 4, 2 ( 2010 ). Colas Le Guernic and Antoine Girard. 2010. Reachability analysis of linear systems using support functions. Nonlinear Analysis: Hybrid Systems 4, 2 (2010)."},{"key":"e_1_3_2_1_40_1","unstructured":"Alexander V Lotov Vladimir A Bushenkov and Georgy K Kamenev. 2013. Interactive decision maps: Approximation and visualization of Pareto frontier.  Alexander V Lotov Vladimir A Bushenkov and Georgy K Kamenev. 2013. Interactive decision maps: Approximation and visualization of Pareto frontier."},{"key":"e_1_3_2_1_41_1","volume-title":"Workshop\/School\/Symposium of the REX Project.","author":"Maler Oded","year":"1991","unstructured":"Oded Maler , Zohar Manna , and Amir Pnueli . 1991 . From timed to hybrid systems . In Workshop\/School\/Symposium of the REX Project. Oded Maler, Zohar Manna, and Amir Pnueli. 1991. From timed to hybrid systems. In Workshop\/School\/Symposium of the REX Project."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/646880.710472"},{"key":"e_1_3_2_1_43_1","series-title":"SIAM review 45, 1","volume-title":"Nineteen dubious ways to compute the exponential of a matrix, twenty-five years later","author":"Moler Cleve","year":"2003","unstructured":"Cleve Moler and Charles Van Loan . 2003. Nineteen dubious ways to compute the exponential of a matrix, twenty-five years later . SIAM review 45, 1 ( 2003 ), 3--49. Cleve Moler and Charles Van Loan. 2003. Nineteen dubious ways to compute the exponential of a matrix, twenty-five years later. SIAM review 45, 1 (2003), 3--49."},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2168773.2168781"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-88562-7_19"},{"key":"e_1_3_2_1_47_1","volume-title":"Proc. IEEE","author":"Tomlin C.J.","year":"2003","unstructured":"C.J. Tomlin , I. Mitchell , A.M. Bayen , and M. Oishi . 2003. Computational techniques for the verification of hybrid systems . Proc. IEEE ( 2003 ). C.J. Tomlin, I. Mitchell, A.M. Bayen, and M. Oishi. 2003. Computational techniques for the verification of hybrid systems. Proc. IEEE (2003)."},{"key":"e_1_3_2_1_48_1","volume-title":"3rd Applied Verification for Continuous and Hybrid Systems Workshop (ARCH)","author":"Tran Hoang-Dung","year":"2016","unstructured":"Hoang-Dung Tran , Luan Viet Nguyen , and Taylor T Johnson . 2016 . Large-scale linear systems from order-reduction (benchmark proposal) . In 3rd Applied Verification for Continuous and Hybrid Systems Workshop (ARCH) , Vienna, Austria. Hoang-Dung Tran, Luan Viet Nguyen, and Taylor T Johnson. 2016. Large-scale linear systems from order-reduction (benchmark proposal). In 3rd Applied Verification for Continuous and Hybrid Systems Workshop (ARCH), Vienna, Austria."},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10626-017-0244-y"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"crossref","unstructured":"Lloyd N Trefethen and David Bau III. 1997. Numerical linear algebra. SIAM.  Lloyd N Trefethen and David Bau III. 1997. Numerical linear algebra. SIAM.","DOI":"10.1137\/1.9780898719574"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1137\/16M1063733"}],"event":{"name":"HSCC '19: 22nd ACM International Conference on Hybrid Systems: Computation and Control","location":"Montreal Quebec Canada","acronym":"HSCC '19","sponsor":["SIGBED ACM Special Interest Group on Embedded Systems"]},"container-title":["Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3302504.3311792","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3302504.3311792","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3302504.3311792","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:25:36Z","timestamp":1750206336000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3302504.3311792"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,4,16]]},"references-count":48,"alternative-id":["10.1145\/3302504.3311792","10.1145\/3302504"],"URL":"https:\/\/doi.org\/10.1145\/3302504.3311792","relation":{},"subject":[],"published":{"date-parts":[[2019,4,16]]},"assertion":[{"value":"2019-04-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}