[{"author":[{"first_name":"Nils","last_name":"Froleyks","full_name":"Froleyks, Nils"},{"orcid":"0000-0002-4993-773X","full_name":"Yu, Zhengqi","id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342","first_name":"Zhengqi","last_name":"Yu"},{"first_name":"Mathias","last_name":"Preiner","full_name":"Preiner, Mathias"},{"full_name":"Biere, Armin","first_name":"Armin","last_name":"Biere"},{"last_name":"Heljanko","first_name":"Keijo","full_name":"Heljanko, Keijo"}],"external_id":{"isi":["001562507100014"]},"isi":1,"OA_place":"publisher","oa_version":"Published Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","acknowledgement":"This work is supported in part by the ERC-2020-AdG 101020093, the LIT AI Lab funded by the State of Upper Austria, the Research Council of Finland under the project 336092, and a gift from Intel Corporation.\r\nFurthermore we of course also owe a big thank-you to the submitters of model checkers and benchmarks to the competition over all these years. Without their enthusiasm and support neither the competition nor this study would exist.","has_accepted_license":"1","file":[{"file_id":"20266","date_updated":"2025-09-02T05:46:10Z","creator":"dernst","content_type":"application/pdf","date_created":"2025-09-02T05:46:10Z","relation":"main_file","access_level":"open_access","file_size":1078274,"checksum":"15ec1bc9b9409d3b2736f4c9d5f42fd1","success":1,"file_name":"2025_CAV_Froleyks.pdf"}],"publisher":"Springer Nature","citation":{"ama":"Froleyks N, Yu E, Preiner M, Biere A, Heljanko K. Introducing certificates to the hardware model checking competition. In: <i>37th International Conference on Computer Aided Verification</i>. Vol 15931. Springer Nature; 2025:281-295. doi:<a href=\"https://doi.org/10.1007/978-3-031-98668-0_14\">10.1007/978-3-031-98668-0_14</a>","ieee":"N. Froleyks, E. Yu, M. Preiner, A. Biere, and K. Heljanko, “Introducing certificates to the hardware model checking competition,” in <i>37th International Conference on Computer Aided Verification</i>, Zagreb, Croatia, 2025, vol. 15931, pp. 281–295.","apa":"Froleyks, N., Yu, E., Preiner, M., Biere, A., &#38; Heljanko, K. (2025). Introducing certificates to the hardware model checking competition. In <i>37th International Conference on Computer Aided Verification</i> (Vol. 15931, pp. 281–295). Zagreb, Croatia: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-98668-0_14\">https://doi.org/10.1007/978-3-031-98668-0_14</a>","ista":"Froleyks N, Yu E, Preiner M, Biere A, Heljanko K. 2025. Introducing certificates to the hardware model checking competition. 37th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 15931, 281–295.","mla":"Froleyks, Nils, et al. “Introducing Certificates to the Hardware Model Checking Competition.” <i>37th International Conference on Computer Aided Verification</i>, vol. 15931, Springer Nature, 2025, pp. 281–95, doi:<a href=\"https://doi.org/10.1007/978-3-031-98668-0_14\">10.1007/978-3-031-98668-0_14</a>.","short":"N. Froleyks, E. Yu, M. Preiner, A. Biere, K. Heljanko, in:, 37th International Conference on Computer Aided Verification, Springer Nature, 2025, pp. 281–295.","chicago":"Froleyks, Nils, Emily Yu, Mathias Preiner, Armin Biere, and Keijo Heljanko. “Introducing Certificates to the Hardware Model Checking Competition.” In <i>37th International Conference on Computer Aided Verification</i>, 15931:281–95. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-98668-0_14\">https://doi.org/10.1007/978-3-031-98668-0_14</a>."},"department":[{"_id":"ToHe"}],"date_created":"2025-08-17T22:01:36Z","page":"281-295","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"status":"public","month":"01","date_published":"2025-01-01T00:00:00Z","project":[{"call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093"}],"quality_controlled":"1","publication_identifier":{"isbn":["9783031986673"],"eissn":["1611-3349"],"issn":["0302-9743"]},"intvolume":"     15931","_id":"20189","ec_funded":1,"file_date_updated":"2025-09-02T05:46:10Z","publication_status":"published","doi":"10.1007/978-3-031-98668-0_14","volume":15931,"title":"Introducing certificates to the hardware model checking competition","alternative_title":["LNCS"],"year":"2025","day":"01","OA_type":"hybrid","conference":{"name":"CAV: Computer Aided Verification","end_date":"2025-07-25","location":"Zagreb, Croatia","start_date":"2025-07-23"},"oa":1,"abstract":[{"text":"Certification was made mandatory for the first time in the latest hardware model checking competition. In this case study, we investigate the trade-offs of requiring certificates for both passing and failing properties in the competition. Our evaluation shows that participating model checkers were able to produce compact, correct certificates that could be verified with minimal overhead. Furthermore, the certifying winner of the competition outperforms the previous non-certifying state-of-the-art model checker, demonstrating that certification can be adopted without compromising model checking efficiency.","lang":"eng"}],"language":[{"iso":"eng"}],"article_processing_charge":"Yes (in subscription journal)","date_updated":"2025-12-01T12:34:05Z","type":"conference","publication":"37th International Conference on Computer Aided Verification","ddc":["000"],"scopus_import":"1"},{"ddc":["000"],"scopus_import":"1","date_updated":"2025-09-03T10:37:59Z","type":"conference","publication":"7th Annual Learning for Dynamics & Control Conference","article_processing_charge":"No","corr_author":"1","abstract":[{"text":"We study the problem of predictive runtime monitoring of black-box dynamical systems with quantitative safety properties. The black-box setting stipulates that the exact semantics of the dynamical system and the controller are unknown, and that we are only able to observe the state of the controlled (aka, closed-loop) system at finitely many time points. We present a novel framework for predicting future states of the system based on the states observed in the past. The numbers of past states and of predicted future states are parameters provided by the user. Our method is based on a combination of Taylor’s expansion and the backward difference operator for numerical differentiation. We also derive an upper bound on the prediction error under the assumption that the system dynamics and the controller are smooth. The predicted states are then used to predict safety violations ahead in time. Our experiments demonstrate practical applicability of our method for complex black-box systems, showing that it is computationally lightweight and yet significantly more accurate than the state-of-the-art predictive safety monitoring techniques.","lang":"eng"}],"language":[{"iso":"eng"}],"title":"Predictive monitoring of black-box dynamical systems","volume":283,"alternative_title":["PMLR"],"year":"2025","day":"01","OA_type":"gold","conference":{"name":"L4DC: Learning for Dynamics & Control","end_date":"2025-06-06","location":"Ann Arbor, MI, United States","start_date":"2025-06-04"},"oa":1,"publication_status":"published","ec_funded":1,"file_date_updated":"2025-09-03T10:32:12Z","intvolume":"       283","publication_identifier":{"eissn":["2640-3498"]},"_id":"20256","date_published":"2025-06-01T00:00:00Z","project":[{"name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","grant_number":"101020093"}],"quality_controlled":"1","page":"804-816","status":"public","month":"06","publisher":"ML Research Press","citation":{"apa":"Henzinger, T. A., Kresse, F., Mallik, K., Yu, E., &#38; Zikelic, D. (2025). Predictive monitoring of black-box dynamical systems. In <i>7th Annual Learning for Dynamics &#38; Control Conference</i> (Vol. 283, pp. 804–816). Ann Arbor, MI, United States: ML Research Press.","ieee":"T. A. Henzinger, F. Kresse, K. Mallik, E. Yu, and D. Zikelic, “Predictive monitoring of black-box dynamical systems,” in <i>7th Annual Learning for Dynamics &#38; Control Conference</i>, Ann Arbor, MI, United States, 2025, vol. 283, pp. 804–816.","ama":"Henzinger TA, Kresse F, Mallik K, Yu E, Zikelic D. Predictive monitoring of black-box dynamical systems. In: <i>7th Annual Learning for Dynamics &#38; Control Conference</i>. Vol 283. ML Research Press; 2025:804-816.","chicago":"Henzinger, Thomas A, Fabian Kresse, Kaushik Mallik, Emily Yu, and Dorde Zikelic. “Predictive Monitoring of Black-Box Dynamical Systems.” In <i>7th Annual Learning for Dynamics &#38; Control Conference</i>, 283:804–16. ML Research Press, 2025.","ista":"Henzinger TA, Kresse F, Mallik K, Yu E, Zikelic D. 2025. Predictive monitoring of black-box dynamical systems. 7th Annual Learning for Dynamics &#38; Control Conference. L4DC: Learning for Dynamics &#38; Control, PMLR, vol. 283, 804–816.","short":"T.A. Henzinger, F. Kresse, K. Mallik, E. Yu, D. Zikelic, in:, 7th Annual Learning for Dynamics &#38; Control Conference, ML Research Press, 2025, pp. 804–816.","mla":"Henzinger, Thomas A., et al. “Predictive Monitoring of Black-Box Dynamical Systems.” <i>7th Annual Learning for Dynamics &#38; Control Conference</i>, vol. 283, ML Research Press, 2025, pp. 804–16."},"department":[{"_id":"ToHe"},{"_id":"ChLa"}],"date_created":"2025-08-31T22:01:32Z","has_accepted_license":"1","acknowledgement":"This work was supported in part by the ERC project ERC-2020-AdG 101020093.\r\n","file":[{"creator":"dernst","content_type":"application/pdf","file_id":"20283","date_updated":"2025-09-03T10:32:12Z","success":1,"file_size":489639,"checksum":"d5236e561560635f5ae1d17de4903033","file_name":"2025_L4DC_HenzingerT.pdf","date_created":"2025-09-03T10:32:12Z","relation":"main_file","access_level":"open_access"}],"oa_version":"Published Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"last_name":"Kresse","first_name":"Fabian","full_name":"Kresse, Fabian","id":"faff3c84-23f6-11ef-9085-e5187b51c604"},{"id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","full_name":"Mallik, Kaushik","orcid":"0000-0001-9864-7475","last_name":"Mallik","first_name":"Kaushik"},{"last_name":"Yu","first_name":"Zhengqi","id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342","full_name":"Yu, Zhengqi"},{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699","first_name":"Dorde","last_name":"Zikelic"}],"arxiv":1,"external_id":{"arxiv":["2412.16564"]},"OA_place":"publisher"},{"has_accepted_license":"1","acknowledgement":"This work is supported in part by the ERC grant under Grant No. ERC-2020-AdG 101020093 and\r\nthe Austrian Science Fund (FWF) [10.55776/COE12]. This research was supported by the Scientific\r\nService Units (SSU) of ISTA through resources provided by Scientific Computing (SciComp).","file":[{"success":1,"checksum":"90a32defed34787e771a5c1623b6b0d2","file_size":295466,"file_name":"2025_NeuS_Kresse.pdf","relation":"main_file","access_level":"open_access","date_created":"2025-09-09T08:10:13Z","content_type":"application/pdf","creator":"dernst","file_id":"20314","date_updated":"2025-09-09T08:10:13Z"}],"oa_version":"Published Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","OA_place":"publisher","author":[{"first_name":"Fabian","last_name":"Kresse","full_name":"Kresse, Fabian","id":"faff3c84-23f6-11ef-9085-e5187b51c604"},{"full_name":"Yu, Zhengqi","id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342","last_name":"Yu","first_name":"Zhengqi"},{"id":"40C20FD2-F248-11E8-B48F-1D18A9856A87","full_name":"Lampert, Christoph","orcid":"0000-0001-8622-7887","last_name":"Lampert","first_name":"Christoph"},{"full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A"}],"external_id":{"arxiv":["2505.19932"]},"arxiv":1,"publication_identifier":{"eissn":["2640-3498"]},"intvolume":"       288","_id":"20296","quality_controlled":"1","project":[{"call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093"}],"date_published":"2025-06-01T00:00:00Z","status":"public","month":"06","department":[{"_id":"ChLa"},{"_id":"ToHe"}],"date_created":"2025-09-07T22:01:34Z","citation":{"ama":"Kresse F, Yu E, Lampert C, Henzinger TA. Logic gate neural networks are good for verification. In: <i>2nd International Conferenceon Neuro-Symbolic Systems</i>. Vol 288. ML Research Press; 2025.","ieee":"F. Kresse, E. Yu, C. Lampert, and T. A. Henzinger, “Logic gate neural networks are good for verification,” in <i>2nd International Conferenceon Neuro-Symbolic Systems</i>, Philadephia, PA, United States, 2025, vol. 288.","apa":"Kresse, F., Yu, E., Lampert, C., &#38; Henzinger, T. A. (2025). Logic gate neural networks are good for verification. In <i>2nd International Conferenceon Neuro-Symbolic Systems</i> (Vol. 288). Philadephia, PA, United States: ML Research Press.","ista":"Kresse F, Yu E, Lampert C, Henzinger TA. 2025. Logic gate neural networks are good for verification. 2nd International Conferenceon Neuro-Symbolic Systems. NeuS: International Conferenceon Neuro-Symbolic Systems, PMLR, vol. 288, 26.","short":"F. Kresse, E. Yu, C. Lampert, T.A. Henzinger, in:, 2nd International Conferenceon Neuro-Symbolic Systems, ML Research Press, 2025.","mla":"Kresse, Fabian, et al. “Logic Gate Neural Networks Are Good for Verification.” <i>2nd International Conferenceon Neuro-Symbolic Systems</i>, vol. 288, 26, ML Research Press, 2025.","chicago":"Kresse, Fabian, Emily Yu, Christoph Lampert, and Thomas A Henzinger. “Logic Gate Neural Networks Are Good for Verification.” In <i>2nd International Conferenceon Neuro-Symbolic Systems</i>, Vol. 288. ML Research Press, 2025."},"publisher":"ML Research Press","language":[{"iso":"eng"}],"article_number":"26","acknowledged_ssus":[{"_id":"ScienComp"}],"abstract":[{"text":"Learning-based systems are increasingly deployed across various domains, yet the complexity of traditional neural networks poses significant challenges for formal verification. Unlike conventional neural networks, learned Logic Gate Networks (LGNs) replace multiplications with Boolean logic gates, yielding a sparse, netlist-like architecture that is inherently more amenable to symbolic verification, while still delivering promising performance. In this paper, we introduce a SAT encoding for verifying global robustness and fairness in LGNs. We evaluate our method on five benchmark datasets, including a newly constructed 5-class variant, and find that LGNs are both verification-friendly and maintain strong predictive performance.","lang":"eng"}],"corr_author":"1","conference":{"start_date":"2025-05-28","name":"NeuS: International Conferenceon Neuro-Symbolic Systems","end_date":"2025-05-30","location":"Philadephia, PA, United States"},"OA_type":"diamond","day":"01","oa":1,"title":"Logic gate neural networks are good for verification","volume":288,"year":"2025","alternative_title":["PMLR"],"publication_status":"published","file_date_updated":"2025-09-09T08:10:13Z","ec_funded":1,"ddc":["000"],"scopus_import":"1","date_updated":"2025-09-09T08:12:44Z","publication":"2nd International Conferenceon Neuro-Symbolic Systems","type":"conference","article_processing_charge":"No"},{"article_processing_charge":"No","scopus_import":"1","publication":"Proceedings of the 39th AAAI Conference on Artificial Intelligence","type":"conference","date_updated":"2025-05-12T09:49:25Z","publication_status":"published","doi":"10.1609/aaai.v39i25.34840","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2412.12996"}],"ec_funded":1,"corr_author":"1","abstract":[{"text":"Learning-based methods provide a promising approach to solving highly non-linear control tasks that are often challenging for classical control methods. To ensure the satisfaction of a safety property, learning-based methods jointly learn a control policy together with a certificate function for the property. Popular examples include barrier functions for safety and Lyapunov functions for asymptotic stability. While there has been significant progress on learning-based control with certificate functions in the white-box setting, where the correctness of the certificate function can be formally verified, there has been little work on ensuring their reliability in the black-box setting where the system dynamics are unknown. In this work, we consider the problems of certifying and repairing neural network control policies and certificate functions in the black-box setting. We propose a novel framework that utilizes runtime monitoring to detect system behaviors that violate the property of interest under some initially trained neural network policy and certificate. These violating behaviors are used to extract new training data, that is used to re-train the neural network policy and the certificate function and to ultimately repair them. We demonstrate the effectiveness of our approach empirically by using it to repair and to boost the safety rate of neural network policies learned by a state-of-the-art method for learning-based control on two autonomous system control tasks.","lang":"eng"}],"language":[{"iso":"eng"}],"year":"2025","title":"Neural control and certificate repair via runtime monitoring","volume":39,"oa":1,"conference":{"start_date":"2025-02-25","end_date":"2025-03-04","location":"Philadelphia, PA, United States","name":"AAAI: Conference on Artificial Intelligence"},"day":"11","OA_type":"green","page":"26409-26417","month":"04","status":"public","publisher":"Association for the Advancement of Artificial Intelligence","citation":{"ama":"Yu E, Zikelic D, Henzinger TA. Neural control and certificate repair via runtime monitoring. In: <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>. Vol 39. Association for the Advancement of Artificial Intelligence; 2025:26409-26417. doi:<a href=\"https://doi.org/10.1609/aaai.v39i25.34840\">10.1609/aaai.v39i25.34840</a>","apa":"Yu, E., Zikelic, D., &#38; Henzinger, T. A. (2025). Neural control and certificate repair via runtime monitoring. In <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i> (Vol. 39, pp. 26409–26417). Philadelphia, PA, United States: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v39i25.34840\">https://doi.org/10.1609/aaai.v39i25.34840</a>","ieee":"E. Yu, D. Zikelic, and T. A. Henzinger, “Neural control and certificate repair via runtime monitoring,” in <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, Philadelphia, PA, United States, 2025, vol. 39, no. 25, pp. 26409–26417.","chicago":"Yu, Emily, Dorde Zikelic, and Thomas A Henzinger. “Neural Control and Certificate Repair via Runtime Monitoring.” In <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, 39:26409–17. Association for the Advancement of Artificial Intelligence, 2025. <a href=\"https://doi.org/10.1609/aaai.v39i25.34840\">https://doi.org/10.1609/aaai.v39i25.34840</a>.","ista":"Yu E, Zikelic D, Henzinger TA. 2025. Neural control and certificate repair via runtime monitoring. Proceedings of the 39th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 39, 26409–26417.","mla":"Yu, Emily, et al. “Neural Control and Certificate Repair via Runtime Monitoring.” <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, vol. 39, no. 25, Association for the Advancement of Artificial Intelligence, 2025, pp. 26409–17, doi:<a href=\"https://doi.org/10.1609/aaai.v39i25.34840\">10.1609/aaai.v39i25.34840</a>.","short":"E. Yu, D. Zikelic, T.A. Henzinger, in:, Proceedings of the 39th AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2025, pp. 26409–26417."},"date_created":"2025-05-11T22:02:40Z","department":[{"_id":"ToHe"}],"_id":"19668","publication_identifier":{"eissn":["2374-3468"],"issn":["2159-5399"]},"intvolume":"        39","issue":"25","date_published":"2025-04-11T00:00:00Z","quality_controlled":"1","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Preprint","external_id":{"arxiv":["2412.12996"]},"arxiv":1,"author":[{"id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342","full_name":"Yu, Zhengqi","first_name":"Zhengqi","last_name":"Yu"},{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699","first_name":"Dorde","last_name":"Zikelic"},{"orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"}],"OA_place":"repository","acknowledgement":"This work was supported in part by the ERC project ERC2020-AdG 101020093"},{"acknowledgement":"This work is supported by the European Research Council under Grant No.: ERC-2020-AdG 101020093.","oa_version":"Preprint","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"last_name":"Kueffner","first_name":"Konstantin","id":"8121a2d0-dc85-11ea-9058-af578f3b4515","orcid":"0000-0001-8974-2542","full_name":"Kueffner, Konstantin"},{"first_name":"Zhengqi","last_name":"Yu","orcid":"0000-0002-4993-773X","full_name":"Yu, Zhengqi","id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342"}],"external_id":{"arxiv":["2507.11987"]},"arxiv":1,"OA_place":"repository","publication_identifier":{"eisbn":["9783032054357"],"issn":["0302-9743"],"eissn":["1611-3349"]},"intvolume":"     16087","_id":"21091","date_published":"2025-09-13T00:00:00Z","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}],"quality_controlled":"1","page":"54-72","status":"public","month":"09","citation":{"chicago":"Henzinger, Thomas A, Konstantin Kueffner, and Emily Yu. “Formal Verification of Neural Certificates Done Dynamically.” In <i>25th International Conference on Runtime Verification</i>, 16087:54–72. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-032-05435-7_4\">https://doi.org/10.1007/978-3-032-05435-7_4</a>.","short":"T.A. Henzinger, K. Kueffner, E. Yu, in:, 25th International Conference on Runtime Verification, Springer Nature, 2025, pp. 54–72.","mla":"Henzinger, Thomas A., et al. “Formal Verification of Neural Certificates Done Dynamically.” <i>25th International Conference on Runtime Verification</i>, vol. 16087, Springer Nature, 2025, pp. 54–72, doi:<a href=\"https://doi.org/10.1007/978-3-032-05435-7_4\">10.1007/978-3-032-05435-7_4</a>.","ista":"Henzinger TA, Kueffner K, Yu E. 2025. Formal verification of neural certificates done dynamically. 25th International Conference on Runtime Verification. RV: Runtime Verification, LNCS, vol. 16087, 54–72.","ama":"Henzinger TA, Kueffner K, Yu E. Formal verification of neural certificates done dynamically. In: <i>25th International Conference on Runtime Verification</i>. Vol 16087. Springer Nature; 2025:54-72. doi:<a href=\"https://doi.org/10.1007/978-3-032-05435-7_4\">10.1007/978-3-032-05435-7_4</a>","ieee":"T. A. Henzinger, K. Kueffner, and E. Yu, “Formal verification of neural certificates done dynamically,” in <i>25th International Conference on Runtime Verification</i>, Graz, Austria, 2025, vol. 16087, pp. 54–72.","apa":"Henzinger, T. A., Kueffner, K., &#38; Yu, E. (2025). Formal verification of neural certificates done dynamically. In <i>25th International Conference on Runtime Verification</i> (Vol. 16087, pp. 54–72). Graz, Austria: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-032-05435-7_4\">https://doi.org/10.1007/978-3-032-05435-7_4</a>"},"publisher":"Springer Nature","department":[{"_id":"ToHe"}],"date_created":"2026-01-29T16:03:01Z","corr_author":"1","abstract":[{"lang":"eng","text":"Neural certificates have emerged as a powerful tool in cyber-physical systems control, providing witnesses of correctness. These certificates, such as barrier functions, often learned alongside control policies, once verified, serve as mathematical proofs of system safety. However, traditional formal verification of their defining conditions typically faces scalability challenges due to exhaustive state-space exploration. To address this challenge, we propose a lightweight runtime monitoring framework that integrates real-time verification and does not require access to the underlying control policy. Our monitor observes the system during deployment and performs on-the-fly verification of the certificate over a lookahead region to ensure safety within a finite prediction horizon. We instantiate this framework for ReLU-based control barrier functions and demonstrate its practical effectiveness in a case study. Our approach enables timely detection of safety violations and incorrect certificates with minimal overhead, providing an effective but lightweight alternative to the static verification of the certificates."}],"language":[{"iso":"eng"}],"volume":16087,"title":"Formal verification of neural certificates done dynamically","year":"2025","alternative_title":["LNCS"],"OA_type":"green","day":"13","conference":{"name":"RV: Runtime Verification","location":"Graz, Austria","end_date":"2025-09-19","start_date":"2025-09-15"},"oa":1,"publication_status":"published","doi":"10.1007/978-3-032-05435-7_4","ec_funded":1,"main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2507.11987","open_access":"1"}],"date_updated":"2026-02-16T11:53:25Z","publication":"25th International Conference on Runtime Verification","type":"conference","article_processing_charge":"No"},{"article_processing_charge":"No","scopus_import":"1","type":"conference","publication":"27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems","date_updated":"2026-01-05T14:05:35Z","publication_status":"published","main_file_link":[{"url":"https://cca.informatik.uni-freiburg.de/papers/FroleyksYuBiere-MBMV24.pdf","open_access":"1"}],"ec_funded":1,"language":[{"iso":"eng"}],"abstract":[{"text":"We introduce a formalization of ternary simulation as abstract interpretation along with a widening operator to speed up convergence. With the same goal, we present a subsumption algorithm that can determine termination earlier than the usual approach using hash sets. Additionally, we introduce a narrowing operator that utilizes recent advances in backbone extraction, allowing to increase the overapproximation precision in simulation at any time. The experiments evaluate the presented techniques in the context of hardware model checking.","lang":"eng"}],"oa":1,"day":"01","OA_type":"green","conference":{"location":"Kaiserslautern, Germany","name":"MBMV: Methods and Description Languages for Modeling and Verification of Circuits and Systems","end_date":"2024-02-15","start_date":"2024-02-14"},"year":"2024","title":"Ternary simulation as abstract interpretation (Work in Progress)","month":"02","status":"public","page":"148-151","date_created":"2024-05-26T22:00:58Z","department":[{"_id":"ToHe"}],"citation":{"ieee":"N. Froleyks, E. Yu, and A. Biere, “Ternary simulation as abstract interpretation (Work in Progress),” in <i>27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems</i>, Kaiserslautern, Germany, 2024, pp. 148–151.","ama":"Froleyks N, Yu E, Biere A. Ternary simulation as abstract interpretation (Work in Progress). In: <i>27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems</i>. ; 2024:148-151.","apa":"Froleyks, N., Yu, E., &#38; Biere, A. (2024). Ternary simulation as abstract interpretation (Work in Progress). In <i>27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems</i> (pp. 148–151). Kaiserslautern, Germany.","ista":"Froleyks N, Yu E, Biere A. 2024. Ternary simulation as abstract interpretation (Work in Progress). 27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems. MBMV: Methods and Description Languages for Modeling and Verification of Circuits and Systems, 148–151.","mla":"Froleyks, Nils, et al. “Ternary Simulation as Abstract Interpretation (Work in Progress).” <i>27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems</i>, 2024, pp. 148–51.","short":"N. Froleyks, E. Yu, A. Biere, in:, 27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems, 2024, pp. 148–151.","chicago":"Froleyks, Nils, Emily Yu, and Armin Biere. “Ternary Simulation as Abstract Interpretation (Work in Progress).” In <i>27th Workshop on Methods and Description Languages for Modeling and Verification of Circuits and Systems</i>, 148–51, 2024."},"_id":"17053","publication_identifier":{"isbn":["9783800762682"]},"quality_controlled":"1","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}],"date_published":"2024-02-01T00:00:00Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa_version":"Submitted Version","OA_place":"repository","author":[{"full_name":"Froleyks, Nils","last_name":"Froleyks","first_name":"Nils"},{"last_name":"Yu","first_name":"Zhengqi","id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342","orcid":"0000-0002-4993-773X","full_name":"Yu, Zhengqi"},{"full_name":"Biere, Armin","first_name":"Armin","last_name":"Biere"}],"acknowledgement":"This work is supported by the Austrian Science Fund (FWF) under the project W1255-N23, the LIT AI Lab funded by the State of Upper Austria, the ERC-2020-AdG 101020093 and by a gift from Intel Corporation."},{"oa_version":"Published Version","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","isi":1,"author":[{"first_name":"Nils","last_name":"Froleyks","full_name":"Froleyks, Nils"},{"full_name":"Yu, Zhengqi","id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342","last_name":"Yu","first_name":"Zhengqi"},{"full_name":"Biere, Armin","first_name":"Armin","last_name":"Biere"},{"first_name":"Keijo","last_name":"Heljanko","full_name":"Heljanko, Keijo"}],"arxiv":1,"external_id":{"arxiv":["2405.04297"],"isi":["001273489700017"]},"acknowledgement":"This work is supported by the Austrian Science Fund (FWF) under the project W1255-N23, the LIT AI Lab funded by the State of Upper Austria, the ERC-2020-AdG 101020093, the Academy of Finland under the project 336092 and by a gift from Intel Corporation.","has_accepted_license":"1","file":[{"file_id":"17414","date_updated":"2024-08-12T06:53:39Z","content_type":"application/pdf","creator":"dernst","relation":"main_file","access_level":"open_access","date_created":"2024-08-12T06:53:39Z","file_size":556902,"checksum":"7d7839fc8c5c680ea3ac09f40a66e55d","success":1,"file_name":"2024_LNCS_Froleyks.pdf"}],"status":"public","month":"07","page":"284-303","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","short":"CC BY (4.0)"},"department":[{"_id":"ToHe"}],"date_created":"2024-08-11T22:01:13Z","citation":{"ista":"Froleyks N, Yu E, Biere A, Heljanko K. 2024. Certifying phase abstraction. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). IJCAR: International Joint Conference on Automated Reasoning, LNCS, vol. 14739, 284–303.","mla":"Froleyks, Nils, et al. “Certifying Phase Abstraction.” <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, vol. 14739, Springer Nature, 2024, pp. 284–303, doi:<a href=\"https://doi.org/10.1007/978-3-031-63498-7_17\">10.1007/978-3-031-63498-7_17</a>.","short":"N. Froleyks, E. Yu, A. Biere, K. Heljanko, in:, Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer Nature, 2024, pp. 284–303.","chicago":"Froleyks, Nils, Emily Yu, Armin Biere, and Keijo Heljanko. “Certifying Phase Abstraction.” In <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, 14739:284–303. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-63498-7_17\">https://doi.org/10.1007/978-3-031-63498-7_17</a>.","apa":"Froleyks, N., Yu, E., Biere, A., &#38; Heljanko, K. (2024). Certifying phase abstraction. In <i>Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i> (Vol. 14739, pp. 284–303). Nancy, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-63498-7_17\">https://doi.org/10.1007/978-3-031-63498-7_17</a>","ieee":"N. Froleyks, E. Yu, A. Biere, and K. Heljanko, “Certifying phase abstraction,” in <i>Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>, Nancy, France, 2024, vol. 14739, pp. 284–303.","ama":"Froleyks N, Yu E, Biere A, Heljanko K. Certifying phase abstraction. In: <i>Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>. Vol 14739. Springer Nature; 2024:284-303. doi:<a href=\"https://doi.org/10.1007/978-3-031-63498-7_17\">10.1007/978-3-031-63498-7_17</a>"},"publisher":"Springer Nature","intvolume":"     14739","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031634970"]},"_id":"17413","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}],"quality_controlled":"1","date_published":"2024-07-01T00:00:00Z","doi":"10.1007/978-3-031-63498-7_17","publication_status":"published","file_date_updated":"2024-08-12T06:53:39Z","ec_funded":1,"language":[{"iso":"eng"}],"abstract":[{"text":"Certification helps to increase trust in formal verification of safety-critical systems which require assurance on their correctness. In hardware model checking, a widely used formal verification technique, phase abstraction is considered one of the most commonly used preprocessing techniques. We present an approach to certify an extended form of phase abstraction using a generic certificate format. As in earlier works our approach involves constructing a witness circuit with an inductive invariant property that certifies the correctness of the entire model checking process, which is then validated by an independent certificate checker. We have implemented and evaluated the proposed approach including certification for various preprocessing configurations on hardware model checking competition benchmarks. As an improvement on previous work in this area, the proposed method is able to efficiently complete certification with an overhead of a fraction of model checking time.","lang":"eng"}],"day":"01","conference":{"name":"IJCAR: International Joint Conference on Automated Reasoning","end_date":"2024-07-06","location":"Nancy, France","start_date":"2024-07-03"},"oa":1,"volume":14739,"title":"Certifying phase abstraction","alternative_title":["LNCS"],"year":"2024","article_processing_charge":"Yes (in subscription journal)","ddc":["000"],"scopus_import":"1","date_updated":"2025-09-08T08:49:53Z","type":"conference","publication":"Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)"}]