{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,23]],"date-time":"2025-08-23T00:40:08Z","timestamp":1755909608275,"version":"3.44.0"},"publisher-location":"New York, NY, USA","reference-count":40,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,5,14]],"date-time":"2024-05-14T00:00:00Z","timestamp":1715644800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Leading-edge Technology Program of Jiangsu Natural Science Foundation","award":["BK20202001"],"award-info":[{"award-number":["BK20202001"]}]},{"DOI":"10.13039\/501100006374","name":"Fundamental Research Funds for the Central Universities","doi-asserted-by":"publisher","award":["2023300180"],"award-info":[{"award-number":["2023300180"]}],"id":[{"id":"10.13039\/501100006374","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100006374","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["62232008,62172200"],"award-info":[{"award-number":["62232008,62172200"]}],"id":[{"id":"10.13039\/501100006374","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,5,14]]},"DOI":"10.1145\/3641513.3650138","type":"proceedings-article","created":{"date-parts":[[2024,5,2]],"date-time":"2024-05-02T18:05:48Z","timestamp":1714673148000},"page":"1-12","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Poles-based Invariant Generation for Verifying the BIBO Stability of Digital Filters"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1986-6619","authenticated-orcid":false,"given":"Xiao","family":"Guo","sequence":"first","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-7011-7027","authenticated-orcid":false,"given":"Jianhua","family":"Zhao","sequence":"additional","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0517-7801","authenticated-orcid":false,"given":"Lei","family":"Bu","sequence":"additional","affiliation":[{"name":"State Key Laboratory for Novel Software Technology, Nanjing University, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,5,14]]},"reference":[{"volume-title":"Verification, Model Checking, and Abstract Interpretation (Mumbai, India), Deepak D\u2019Souza, Akash Lal, and Kim\u00a0Guldstrand Larsen (Eds.)","author":"Adj\u00e9 Assal\u00e9","unstructured":"Assal\u00e9 Adj\u00e9 and Pierre-Lo\u00efc Garoche. 2015. Automatic Synthesis of Piecewise Linear Quadratic Invariants for Programs. In Verification, Model Checking, and Abstract Interpretation (Mumbai, India), Deepak D\u2019Souza, Akash Lal, and Kim\u00a0Guldstrand Larsen (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 99\u2013116.","key":"e_1_3_2_1_1_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_2_1","DOI":"10.1109\/ASE.2019.00121"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_3_1","DOI":"10.1016\/j.jsc.2017.03.009"},{"key":"e_1_3_2_1_4_1","volume-title":"Progress on Software Verification: SV-COMP","author":"Beyer Dirk","year":"2022","unstructured":"Dirk Beyer. 2022. Progress on Software Verification: SV-COMP 2022. In Tools and Algorithms for the Construction and Analysis of Systems (Munich, Germany), Dana Fisman and Grigore Rosu (Eds.). Springer International Publishing, Cham, 375\u2013402."},{"volume-title":"Computer Aided Verification (Berlin, Germany)","author":"Beyer Dirk","unstructured":"Dirk Beyer, Thomas\u00a0A. Henzinger, and Gr\u00e9gory Th\u00e9oduloz. 2007. Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis. In Computer Aided Verification (Berlin, Germany), Werner Damm and Holger Hermanns (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 504\u2013518.","key":"e_1_3_2_1_5_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_6_1","DOI":"10.1109\/ASE.2008.13"},{"volume-title":"Computer Aided Verification (Snowbird, UT, USA)","author":"Beyer Dirk","unstructured":"Dirk Beyer and M.\u00a0Erkan Keremoglu. 2011. CPAchecker: A Tool for Configurable Software Verification. In Computer Aided Verification (Snowbird, UT, USA), Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 184\u2013190.","key":"e_1_3_2_1_7_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_8_1","DOI":"10.1145\/781131.781153"},{"volume-title":"Static Analysis (Saint-Malo, France)","author":"Cattaruzza Dario","unstructured":"Dario Cattaruzza, Alessandro Abate, Peter Schrammel, and Daniel Kroening. 2015. Unbounded-Time Analysis of Guarded LTI Systems with Inputs by Abstract Acceleration. In Static Analysis (Saint-Malo, France), Sandrine Blazy and Thomas Jensen (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 312\u2013331.","key":"e_1_3_2_1_9_1"},{"volume-title":"Programming Languages and Systems (Edinburgh, UK)","author":"Cousot Patrick","unstructured":"Patrick Cousot, Radhia Cousot, Jer\u00f4me Feret, Laurent Mauborgne, Antoine Min\u00e9, David Monniaux, and Xavier Rival. 2005. The ASTRE\u00c9 Analyzer. In Programming Languages and Systems (Edinburgh, UK), Mooly Sagiv (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 21\u201330.","key":"e_1_3_2_1_10_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_11_1","DOI":"10.7873\/DATE.2015.0245"},{"volume-title":"Formal Methods for Industrial Critical Systems (Eindhoven, The Netherlands), Mar\u00eda Alpuente","author":"Delmas David","unstructured":"David Delmas, Eric Goubault, Sylvie Putot, Jean Souyris, Karim Tekkal, and Franck V\u00e9drine. 2009. Towards an Industrial Use of FLUCTUAT on Safety-Critical Avionics Software. In Formal Methods for Industrial Critical Systems (Eindhoven, The Netherlands), Mar\u00eda Alpuente, Byron Cook, and Christophe Joubert (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 53\u201369.","key":"e_1_3_2_1_12_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_13_1","DOI":"10.4169\/college.math.j.44.2.149"},{"volume-title":"Static Analysis (Venice, Italy)","author":"Donaldson F.","unstructured":"Alastair\u00a0F. Donaldson, Leopold Haller, Daniel Kroening, and Philipp R\u00fcmmer. 2011. Software Verification Using k-Induction. In Static Analysis (Venice, Italy), Eran Yahav (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 351\u2013368.","key":"e_1_3_2_1_14_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_15_1","DOI":"10.2307\/2153450"},{"unstructured":"M.\u00a0Galassi et al. 2009. GNU Scientific Library Reference Manual (3rd Ed.). Network Theory Ltd. Godalming Surrey. http:\/\/www.gnu.org\/software\/gsl\/","key":"e_1_3_2_1_16_1"},{"volume-title":"Programming Languages and Systems (Barcelona, Spain)","author":"Feret J\u00e9r\u00f4me","unstructured":"J\u00e9r\u00f4me Feret. 2004. Static Analysis of Digital Filters. In Programming Languages and Systems (Barcelona, Spain), David Schmidt (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 33\u201348.","key":"e_1_3_2_1_17_1"},{"doi-asserted-by":"crossref","unstructured":"J\u00e9r\u00f4me Feret. 2005. Numerical Abstract Domains for Digital Filters.","key":"e_1_3_2_1_18_1","DOI":"10.1007\/978-3-540-24725-8_4"},{"volume-title":"Hybrid Systems: Computation and Control (Zurich, Switzerland)","author":"Frehse Goran","unstructured":"Goran Frehse. 2005. PHAVer: Algorithmic Verification of Hybrid Systems Past HyTech. In Hybrid Systems: Computation and Control (Zurich, Switzerland), Manfred Morari and Lothar Thiele (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 258\u2013273.","key":"e_1_3_2_1_19_1"},{"volume-title":"Computer Aided Verification (Snowbird, UT, USA)","author":"Frehse Goran","unstructured":"Goran Frehse, Colas Le\u00a0Guernic, 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 Computer Aided Verification (Snowbird, UT, USA), Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 379\u2013395.","key":"e_1_3_2_1_20_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_21_1","DOI":"10.1145\/3238147.3240481"},{"volume-title":"Computer Aided Verification (Grenoble, France)","author":"Ghorbal Khalil","unstructured":"Khalil Ghorbal, Eric Goubault, and Sylvie Putot. 2009. The Zonotope Abstract Domain Taylor1+. In Computer Aided Verification (Grenoble, France), Ahmed Bouajjani and Oded Maler (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 627\u2013633.","key":"e_1_3_2_1_22_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_23_1","DOI":"10.1006\/cviu.1998.0674"},{"volume-title":"Static Analysis (Seoul,Korea)","author":"Gonnord Laure","unstructured":"Laure Gonnord and Nicolas Halbwachs. 2006. Combining Widening and Acceleration in Linear Relation Analysis. In Static Analysis (Seoul,Korea), Kwangkeun Yi (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 144\u2013160.","key":"e_1_3_2_1_24_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_25_1","DOI":"10.1016\/j.scico.2013.09.016"},{"volume-title":"Static Analysis (Seoul, Korea)","author":"Goubault Eric","unstructured":"Eric Goubault and Sylvie Putot. 2006. Static Analysis of Numerical Algorithms. In Static Analysis (Seoul, Korea), Kwangkeun Yi (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 18\u201334.","key":"e_1_3_2_1_26_1"},{"volume-title":"Computer Aided Verification (Haifa, Israel)","author":"Henzinger A.","unstructured":"Thomas\u00a0A. Henzinger, Pei-Hsin Ho, and Howard Wong-Toi. 1997. HyTech: A model checker for hybrid systems. In Computer Aided Verification (Haifa, Israel), Orna Grumberg (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 460\u2013463.","key":"e_1_3_2_1_27_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_28_1","DOI":"10.1145\/2535838.2535843"},{"volume-title":"Linear algebra and its applications. Pearson Education","author":"Lay C","unstructured":"David\u00a0C Lay, Steven\u00a0R Lay, and Judi McDonald. 2016. Linear algebra and its applications. Pearson Education, Upper Saddle River, NJ., USA.","key":"e_1_3_2_1_29_1"},{"volume-title":"Static Analysis (New York","author":"Le\u00a0Guernic Colas","unstructured":"Colas Le\u00a0Guernic. 2017. Toward a Sound Analysis of Guarded LTI Loops with Inputs by Abstract Acceleration. In Static Analysis (New York, NY, USA), Francesco Ranzato (Ed.). Springer International Publishing, Cham, 192\u2013211.","key":"e_1_3_2_1_30_1"},{"volume-title":"Linear Algebra","author":"Martin RS","unstructured":"RS Martin, G Peters, and JH Wilkinson. 1971. The QR algorithm for real Hessenberg matrices. In Linear Algebra. Springer, New York, NY, USA, 359\u2013371.","key":"e_1_3_2_1_31_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_32_1","DOI":"10.1016\/j.jsc.2014.02.001"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_33_1","DOI":"10.1007\/BF02165404"},{"volume-title":"systems, and transforms","author":"Phillips L","unstructured":"Charles\u00a0L Phillips, John\u00a0M Parr, Eve\u00a0Ann Riskin, and Telagarapu Prabhakar. 2003. Signals, systems, and transforms. Prentice Hall, Upper Saddle River, NJ., USA.","key":"e_1_3_2_1_34_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_35_1","DOI":"10.1109\/PROC.1967.5434"},{"volume-title":"FM 2014: Formal Methods","author":"Roux Pierre","unstructured":"Pierre Roux and Pierre-Lo\u00efc Garoche. 2014. Computing Quadratic Invariants with Min- and Max-Policy Iterations: A Practical Comparison. In FM 2014: Formal Methods, Cliff Jones, Pekka Pihlajasaari, and Jun Sun (Eds.). Springer International Publishing, Cham, 563\u2013578.","key":"e_1_3_2_1_36_1"},{"volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (Thessaloniki, Greece)","author":"Roux Pierre","unstructured":"Pierre Roux, Mohamed Iguernlala, and Sylvain Conchon. 2018. A Non-linear Arithmetic Procedure for Control-Command Software Verification. In Tools and Algorithms for the Construction and Analysis of Systems (Thessaloniki, Greece), Dirk Beyer and Marieke Huisman (Eds.). Springer International Publishing, Cham, 132\u2013151.","key":"e_1_3_2_1_37_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_38_1","DOI":"10.1145\/2728606.2728623"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_39_1","DOI":"10.1145\/2185632.2185651"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_40_1","DOI":"10.1145\/992200.992209"}],"event":{"sponsor":["SIGCHI ACM Special Interest Group on Computer-Human Interaction"],"acronym":"HSCC '24","name":"HSCC '24: Computation and Control","location":"Hong Kong SAR China"},"container-title":["Proceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3641513.3650138","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3641513.3650138","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,23]],"date-time":"2025-08-23T00:13:18Z","timestamp":1755907998000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3641513.3650138"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,5,14]]},"references-count":40,"alternative-id":["10.1145\/3641513.3650138","10.1145\/3641513"],"URL":"https:\/\/doi.org\/10.1145\/3641513.3650138","relation":{},"subject":[],"published":{"date-parts":[[2024,5,14]]},"assertion":[{"value":"2024-05-14","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}