{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:52:07Z","timestamp":1742914327642,"version":"3.40.3"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031770180"},{"type":"electronic","value":"9783031770197"}],"license":[{"start":{"date-parts":[[2024,11,22]],"date-time":"2024-11-22T00:00:00Z","timestamp":1732233600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,22]],"date-time":"2024-11-22T00:00:00Z","timestamp":1732233600000},"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":[[2025]]},"DOI":"10.1007\/978-3-031-77019-7_20","type":"book-chapter","created":{"date-parts":[[2024,11,21]],"date-time":"2024-11-21T20:48:15Z","timestamp":1732222095000},"page":"350-367","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Switched Systems in\u00a0Coq for\u00a0Modeling Periodic Controllers"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4717-4206","authenticated-orcid":false,"given":"Andrei","family":"Aleksandrov","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8988-0053","authenticated-orcid":false,"given":"Kim","family":"V\u00f6llinger","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,11,22]]},"reference":[{"key":"20_CR1","doi-asserted-by":"crossref","unstructured":"Abate, C., et al.: SSProve: a foundational framework for modular cryptographic proofs in COQ. In: 2021 IEEE 34th Computer Security Foundations Symposium (CSF), pp. 1\u201315. IEEE (2021)","DOI":"10.1109\/CSF51468.2021.00048"},{"issue":"3","key":"20_CR2","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/s10817-023-09671-5","volume":"67","author":"R Affeldt","year":"2023","unstructured":"Affeldt, R., Cohen, C.: Measure construction by extension in dependent type theory with application to integration. J. Autom. Reason. 67(3), 28 (2023)","journal-title":"J. Autom. Reason."},{"key":"20_CR3","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/978-3-031-33170-1_4","volume-title":"NFM 2023","author":"A Aleksandrov","year":"2023","unstructured":"Aleksandrov, A., V\u00f6llinger, K.: Formalizing piecewise affine activation functions of neural networks in COQ. In: Rozier, K.Y., Chaudhuri, S. (eds.) NFM 2023. LNCS, vol. 13903, pp. 62\u201378. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-33170-1_4"},{"key":"20_CR4","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1146\/annurev-control-071420-081941","volume":"4","author":"M Althoff","year":"2021","unstructured":"Althoff, M., Frehse, G., Girard, A.: Set propagation techniques for reachability analysis. Ann. Rev. Control, Robot. Auton. Syst. 4, 369\u2013395 (2021)","journal-title":"Ann. Rev. Control, Robot. Auton. Syst."},{"issue":"1","key":"20_CR5","doi-asserted-by":"publisher","first-page":"186","DOI":"10.5334\/bc.153","volume":"3","author":"E Belias","year":"2022","unstructured":"Belias, E., Licina, D.: Outdoor PM2. 5 air filtration: optimising indoor air quality and energy. Build. Cities 3(1), 186\u2013203 (2022)","journal-title":"Build. Cities"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Bohrer, R., Rahli, V., Vukotic, I., V\u00f6lp, M., Platzer, A.: Formally verified differential dynamic logic. In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, pp. 208\u2013221 (2017)","DOI":"10.1145\/3018610.3018616"},{"issue":"1","key":"20_CR7","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/s11786-014-0181-1","volume":"9","author":"S Boldo","year":"2015","unstructured":"Boldo, S., Lelay, C., Melquiond, G.: Coquelicot: a user-friendly library of real analysis for Coq. Math. Comput. Sci. 9(1), 41\u201362 (2015)","journal-title":"Math. Comput. Sci."},{"issue":"7","key":"20_CR8","doi-asserted-by":"publisher","first-page":"1196","DOI":"10.1017\/S0960129514000437","volume":"26","author":"S Boldo","year":"2016","unstructured":"Boldo, S., Lelay, C., Melquiond, G.: Formalization of real analysis: a survey of proof assistants and libraries. Math. Struct. Comput. Sci. 26(7), 1196\u20131233 (2016)","journal-title":"Math. Struct. Comput. Sci."},{"issue":"5","key":"20_CR9","doi-asserted-by":"publisher","first-page":"2971","DOI":"10.1002\/rnc.6547","volume":"33","author":"X Chen","year":"2023","unstructured":"Chen, X., Liu, Y., Jiang, B., Lu, J.: Exponential stability of nonlinear switched systems with hybrid delayed impulses. Int. J. Robust Nonlinear Control 33(5), 2971\u20132985 (2023)","journal-title":"Int. J. Robust Nonlinear Control"},{"key":"20_CR10","doi-asserted-by":"publisher","first-page":"104549","DOI":"10.1016\/j.robot.2023.104549","volume":"170","author":"P Crisafulli","year":"2023","unstructured":"Crisafulli, P., Taha, S., Wolff, B.: Modeling and analysing cyber-physical systems in HOL-CSP. Robot. Auton. Syst. 170, 104549 (2023)","journal-title":"Robot. Auton. Syst."},{"key":"#cr-split#-20_CR11.1","unstructured":"Dong, Q., Long, E.: Establishment of mathematical model for indoor particle pollutant concentration change and suggestions on the use of air filters. In: MEMAT 2022"},{"key":"#cr-split#-20_CR11.2","unstructured":"2nd International Conference on Mechanical Engineering, Intelligent Manufacturing and Automation Technology, pp.\u00a01-3. VDE (2022)"},{"key":"20_CR12","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 Syst. Des. 30, 179\u2013198 (2007)","journal-title":"Formal Methods Syst. Des."},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","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\u00a0X: an axiomatic tactical theorem prover for hybrid systems. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 527\u2013538. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_36"},{"key":"20_CR14","doi-asserted-by":"crossref","unstructured":"Gondelman, L., Hinrichsen, J.K., Pereira, M., Timany, A., Birkedal, L.: Verifying reliable network components in a distributed separation logic with dependent separation protocols. Proc. ACM Programm. Lang. 7(ICFP), 847\u2013877 (2023)","DOI":"10.1145\/3607859"},{"key":"20_CR15","doi-asserted-by":"crossref","unstructured":"Liberzon, D.: Basic concepts. In: Switching in Systems and Control, pp. 3\u201315. Birkh\u00e4user Boston, Boston, MA (2003)","DOI":"10.1007\/978-1-4612-0017-8_1"},{"key":"20_CR16","doi-asserted-by":"crossref","unstructured":"Liberzon, D.: Stability under constrained switching. In: Switching in Systems and Control, pp. 53\u201371. Birkh\u00e4user Boston, Boston, MA (2003)","DOI":"10.1007\/978-1-4612-0017-8_3"},{"key":"20_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-030-02450-5_6","volume-title":"Formal Methods and Software Engineering","author":"T Liebrenz","year":"2018","unstructured":"Liebrenz, T., Herber, P., Glesner, S.: Deductive verification of hybrid control systems modeled in simulink with KeYmaera X. In: Sun, J., Sun, M. (eds.) ICFEM 2018. LNCS, vol. 11232, pp. 89\u2013105. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-02450-5_6"},{"key":"20_CR18","doi-asserted-by":"crossref","unstructured":"Logemann, H., Ryan, E.P.: Linear Differential Equations, pp. 21\u201364. Springer, London (2014)","DOI":"10.1007\/978-1-4471-6398-5_2"},{"key":"20_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/978-3-642-39634-2_34","volume-title":"Interactive Theorem Proving","author":"E Makarov","year":"2013","unstructured":"Makarov, E., Spitters, B.: The picard algorithm for ordinary differential equations in Coq. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 463\u2013468. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39634-2_34"},{"key":"20_CR20","doi-asserted-by":"publisher","first-page":"102856","DOI":"10.1016\/j.scico.2022.102856","volume":"222","author":"A Mammar","year":"2022","unstructured":"Mammar, A., Afendi, M., Laleau, R.: Modeling and proving hybrid programs with event-b: an approach by generalization and instantiation. Sci. Comput. Program. 222, 102856 (2022)","journal-title":"Sci. Comput. Program."},{"issue":"4","key":"20_CR21","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/s10817-023-09679-x","volume":"67","author":"\u00c9 Martin-Dorel","year":"2023","unstructured":"Martin-Dorel, \u00c9., Melquiond, G., Roux, P.: Enabling floating-point arithmetic in the coq proof assistant. J. Autom. Reason. 67(4), 33 (2023)","journal-title":"J. Autom. Reason."},{"issue":"7","key":"20_CR22","doi-asserted-by":"publisher","first-page":"4134","DOI":"10.1021\/acs.est.0c03247","volume":"55","author":"ES Mousavi","year":"2021","unstructured":"Mousavi, E.S., Kananizadeh, N., Martinello, R.A., Sherman, J.D.: COVID-19 outbreak and hospital air quality: a systematic review of evidence on air filtration and recirculation. Environ. Sci. Technol. 55(7), 4134\u20134147 (2021)","journal-title":"Environ. Sci. Technol."},{"key":"20_CR23","doi-asserted-by":"crossref","unstructured":"de\u00a0Oliveira\u00a0Oliveira, M., Tveretina, O.: Mortality and edge-to-edge reachability are decidable on surfaces. In: 25th ACM International Conference on Hybrid Systems: Computation and Control, pp. 1\u201310 (2022)","DOI":"10.1145\/3501710.3519529"},{"issue":"2","key":"20_CR24","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s10817-016-9385-1","volume":"59","author":"A Platzer","year":"2016","unstructured":"Platzer, A.: A complete uniform substitution calculus for differential dynamic logic. J. Autom. Reason. 59(2), 219\u2013265 (2016). https:\/\/doi.org\/10.1007\/s10817-016-9385-1","journal-title":"J. Autom. Reason."},{"issue":"1","key":"20_CR25","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3380825","volume":"67","author":"A Platzer","year":"2020","unstructured":"Platzer, A., Tan, Y.K.: Differential equation invariance axiomatization. J. ACM (JACM) 67(1), 1\u201366 (2020)","journal-title":"J. ACM (JACM)"},{"key":"20_CR26","doi-asserted-by":"crossref","unstructured":"Ricketts, D., Malecha, G., Alvarez, M.M., Gowda, V., Lerner, S.: Towards verification of hybrid systems in a foundational proof assistant. In: 2015 ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), pp. 248\u2013257. IEEE (2015)","DOI":"10.1109\/MEMCOD.2015.7340492"},{"key":"20_CR27","doi-asserted-by":"crossref","unstructured":"Rouhling, D.: A formal proof in Coq of a control function for the inverted pendulum. In: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 28\u201341 (2018)","DOI":"10.1145\/3167101"},{"key":"20_CR28","doi-asserted-by":"crossref","unstructured":"Shinnar, A., Trager, B.: General probability in coq. In: 2022 52nd Annual IEEE\/IFIP International Conference on Dependable Systems and Networks Workshops (DSN-W), pp. 70\u201371. IEEE (2022)","DOI":"10.1109\/DSN-W54100.2022.00021"},{"key":"20_CR29","doi-asserted-by":"crossref","unstructured":"Tan, Y.K., Mitsch, S., Platzer, A.: Verifying switched system stability with logic. In: 25th ACM International Conference on Hybrid Systems: Computation and Control, pp. 1\u201311 (2022)","DOI":"10.1145\/3501710.3519541"},{"key":"20_CR30","doi-asserted-by":"publisher","unstructured":"T.C.D., Team: The Coq Proof Assistant (2022). https:\/\/doi.org\/10.5281\/zenodo.7313584","DOI":"10.5281\/zenodo.7313584"},{"key":"20_CR31","unstructured":"Verified Software Toolchain. https:\/\/vst.cs.princeton.edu"},{"issue":"1","key":"20_CR32","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1080\/21642583.2020.1740113","volume":"8","author":"Y Wei","year":"2020","unstructured":"Wei, Y., Jia, S., Liu, K.: A survey on anti-disturbance control of switched systems with input saturation. Syst. Sci. Control Eng. 8(1), 241\u2013248 (2020)","journal-title":"Syst. Sci. Control Eng."},{"key":"20_CR33","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/s10626-014-0187-5","volume":"25","author":"F Zhu","year":"2015","unstructured":"Zhu, F., Antsaklis, P.J.: Optimal control of hybrid switched systems: a brief survey. Discrete Event Dyn. Syst. 25, 345\u2013364 (2015)","journal-title":"Discrete Event Dyn. Syst."}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2024"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-77019-7_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,21]],"date-time":"2024-11-21T21:30:20Z","timestamp":1732224620000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-77019-7_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,22]]},"ISBN":["9783031770180","9783031770197"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-77019-7_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,11,22]]},"assertion":[{"value":"22 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICTAC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Colloquium on Theoretical Aspects of Computing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bangkok","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Thailand","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 November 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 November 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ictac2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ictac2024.cs.ait.ac.th\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}