{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T03:24:05Z","timestamp":1773199445390,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":28,"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:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"EPSRC","award":["EP\/S024050\/1"],"award-info":[{"award-number":["EP\/S024050\/1"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,5,14]]},"DOI":"10.1145\/3641513.3651398","type":"proceedings-article","created":{"date-parts":[[2024,5,2]],"date-time":"2024-05-02T18:05:48Z","timestamp":1714673148000},"page":"1-10","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":22,"title":["Fossil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical Models"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9174-9962","authenticated-orcid":false,"given":"Alec","family":"Edwards","sequence":"first","affiliation":[{"name":"University of Oxford, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7767-2935","authenticated-orcid":false,"given":"Andrea","family":"Peruffo","sequence":"additional","affiliation":[{"name":"Technical University Delft, Netherlands"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5627-9093","authenticated-orcid":false,"given":"Alessandro","family":"Abate","sequence":"additional","affiliation":[{"name":"University of Oxford, United Kingdom"}]}],"member":"320","published-online":{"date-parts":[[2024,5,14]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3447928.3456646"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/LCSYS.2020.3005328"},{"key":"e_1_3_2_1_3_1","unstructured":"Daniel Ahmed Andrea Peruffo and Alessandro Abate. 2018. Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers."},{"key":"e_1_3_2_1_4_1","volume-title":"Feedback systems: an introduction for scientists and engineers","author":"\u00c5str\u00f6m Karl\u00a0Johan","unstructured":"Karl\u00a0Johan \u00c5str\u00f6m and Richard\u00a0M Murray. 2021. Feedback systems: an introduction for scientists and engineers. Princeton university press."},{"key":"e_1_3_2_1_5_1","volume-title":"Principles of model checking","author":"Baier Christel","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of model checking. MIT press."},{"key":"e_1_3_2_1_6_1","volume-title":"Neural lyapunov control. Advances in neural information processing systems 32","author":"Chang Ya-Chien","year":"2019","unstructured":"Ya-Chien Chang, Nima Roohi, and Sicun Gao. 2019. Neural lyapunov control. Advances in neural information processing systems 32 (2019)."},{"key":"e_1_3_2_1_7_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Chatterjee Krishnendu","unstructured":"Krishnendu Chatterjee, Thomas\u00a0A. Henzinger, Mathias Lechner, and \u0110or\u0111e \u017dikeli\u0107. 2023. A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems. In Tools and Algorithms for the Construction and Analysis of Systems, Sriram Sankaranarayanan and Natasha Sharygina (Eds.). Springer Nature Switzerland, Cham, 3\u201325."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2022.3232542"},{"key":"e_1_3_2_1_9_1","unstructured":"Alec Edwards Andrea Peruffo and Alessandro Abate. 2023. Fossil 2.0 Repository. https:\/\/github.com\/oxford-oxcav\/fossil."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Alec Edwards Andrea Peruffo and Alessandro Abate. 2023. A General Verification Framework for Dynamical and Control Models via Certificate Synthesis. arXiv:2309.06090\u00a0[cs eess] arXiv:2309.06090.","DOI":"10.2139\/ssrn.4880686"},{"key":"e_1_3_2_1_11_1","volume-title":"Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems","author":"Gao Sicun","unstructured":"Sicun Gao, James Kapinski, Jyotirmoy Deshmukh, Nima Roohi, Armando Solar-Lezama, Nikos Arechiga, and Soonho Kong. 2019. Numerically-Robust Inductive Proof Rules for Continuous Dynamical Systems. In Computer Aided Verification, Isil Dillig and Serdar Tasiran (Eds.). Springer International Publishing, Cham, 137\u2013154."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/ACCESS.2023.3291349"},{"key":"e_1_3_2_1_13_1","volume-title":"Systematic Synthesis of Passive Fault-Tolerant Augmented Neural Lyapunov Control Laws for Nonlinear Systems. In 2023 62nd IEEE Conference on Decision and Control (CDC).","author":"Grande Davide","year":"2023","unstructured":"Davide Grande, Davide Fenucci, Andrea Peruffo, Enrico Anderlini, Alex\u00a0B Phillips, Thomas Giles, and Georgios Salavasidis. 2023. Systematic Synthesis of Passive Fault-Tolerant Augmented Neural Lyapunov Control Laws for Nonlinear Systems. In 2023 62nd IEEE Conference on Decision and Control (CDC)."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v36i7.20695"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/LCSYS.2022.3229865"},{"key":"e_1_3_2_1_16_1","volume-title":"CoRR abs\/1310.4716","author":"Papachristodoulou Antonis","year":"2013","unstructured":"Antonis Papachristodoulou, James Anderson, Giorgio Valmorbida, Stephen Prajna, Pete Seiler, and Pablo\u00a0A. Parrilo. 2013. SOSTOOLS Version 3.00 Sum of Squares Optimization Toolbox for MATLAB. CoRR abs\/1310.4716 (2013)."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Andrea Peruffo Daniele Ahmed and Alessandro Abate. 2021. Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models. 370\u2013388.","DOI":"10.1007\/978-3-030-72016-2_20"},{"key":"e_1_3_2_1_18_1","first-page":"1","article-title":"Barrier Certificates for Nonlinear Model Validation","volume":"42","author":"Prajna Stephen","year":"2006","unstructured":"Stephen Prajna. 2006. Barrier Certificates for Nonlinear Model Validation. Automatica (Journal of IFAC) 42, 1 (Jan. 2006), 117\u2013126.","journal-title":"Automatica (Journal of IFAC)"},{"key":"e_1_3_2_1_19_1","volume-title":"Stochastic Safety Verification Using Barrier Certificates. In 2004 43rd IEEE Conference on Decision and Control (CDC) (IEEE Cat. No.04CH37601)","volume":"1","author":"Prajna S.","unstructured":"S. Prajna, A. Jadbabaie, and G.J. Pappas. 2004. Stochastic Safety Verification Using Barrier Certificates. In 2004 43rd IEEE Conference on Decision and Control (CDC) (IEEE Cat. No.04CH37601). IEEE, Nassau, Bahamas, 929\u2013934 Vol.1."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-65765-3_17"},{"key":"e_1_3_2_1_21_1","volume-title":"Counterexample Guided Synthesis of Switched Controllers for Reach-While-Stay Properties. CoRR abs\/1505.01180","author":"Ravanbakhsh Hadi","year":"2015","unstructured":"Hadi Ravanbakhsh and Sriram Sankaranarayanan. 2015. Counterexample Guided Synthesis of Switched Controllers for Reach-While-Stay Properties. CoRR abs\/1505.01180 (2015)."},{"key":"e_1_3_2_1_22_1","volume-title":"Stability Analysis and Controller Synthesis using Single-hidden-layer ReLU Neural Networks","author":"Samanipour Pouya","year":"2023","unstructured":"Pouya Samanipour and Hasan\u00a0A. Poonawala. 2023. Stability Analysis and Controller Synthesis using Single-hidden-layer ReLU Neural Networks. IEEE Trans. Automat. Control (2023), 1\u201312."},{"key":"e_1_3_2_1_23_1","volume-title":"Vol.\u00a010","author":"Sastry Shankar","unstructured":"Shankar Sastry. 1999. Nonlinear Systems. Interdisciplinary Applied Mathematics, Vol.\u00a010. Springer New York, New York, NY."},{"key":"e_1_3_2_1_24_1","volume-title":"Mathematical control theory: deterministic finite dimensional systems. Vol.\u00a06","author":"Sontag D","unstructured":"Eduardo\u00a0D Sontag. 2013. Mathematical control theory: deterministic finite dimensional systems. Vol.\u00a06. Springer Science & Business Media."},{"key":"e_1_3_2_1_25_1","volume-title":"Formal controller synthesis for hybrid systems using genetic programming. CoRR abs\/2003.14322","author":"Verdier Cees\u00a0Ferdinand","year":"2020","unstructured":"Cees\u00a0Ferdinand Verdier and Manuel\u00a0Mazo Jr.2020. Formal controller synthesis for hybrid systems using genetic programming. CoRR abs\/2003.14322 (2020)."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.2018.8619121"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3365365.3382222"},{"key":"e_1_3_2_1_28_1","volume-title":"Proceedings of the AAAI Conference on Artificial Intelligence 37","author":"\u017dikeli\u0107 \u0110or\u0111e","year":"2023","unstructured":"\u0110or\u0111e \u017dikeli\u0107, Mathias Lechner, Thomas\u00a0A. Henzinger, and Krishnendu Chatterjee. 2023. Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees. Proceedings of the AAAI Conference on Artificial Intelligence 37, 10 (Jun. 2023), 11926\u201311935. https:\/\/ojs.aaai.org\/index.php\/AAAI\/article\/view\/26407"}],"event":{"name":"HSCC '24: Computation and Control","location":"Hong Kong SAR China","acronym":"HSCC '24","sponsor":["SIGCHI ACM Special Interest Group on Computer-Human Interaction"]},"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.3651398","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3641513.3651398","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,23]],"date-time":"2025-08-23T00:13:10Z","timestamp":1755907990000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3641513.3651398"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,5,14]]},"references-count":28,"alternative-id":["10.1145\/3641513.3651398","10.1145\/3641513"],"URL":"https:\/\/doi.org\/10.1145\/3641513.3651398","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"}}]}}