[{"quality_controlled":"1","oa":1,"project":[{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"},{"_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e","name":"Interface Theory for Security and Privacy","grant_number":"F8502"}],"doi":"10.1145/3719027.3765137","citation":{"ista":"Henzinger TA, Karimi M, Thejaswini KS. 2025. Privacy-preserving runtime verification. Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security. CCS: Conference on Computer and Communications Security, 2774–2787.","apa":"Henzinger, T. A., Karimi, M., &#38; Thejaswini, K. S. (2025). Privacy-preserving runtime verification. In <i>Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security</i> (pp. 2774–2787). Taipei, Taiwan: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3719027.3765137\">https://doi.org/10.1145/3719027.3765137</a>","ama":"Henzinger TA, Karimi M, Thejaswini KS. Privacy-preserving runtime verification. In: <i>Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security</i>. Association for Computing Machinery; 2025:2774-2787. doi:<a href=\"https://doi.org/10.1145/3719027.3765137\">10.1145/3719027.3765137</a>","ieee":"T. A. Henzinger, M. Karimi, and K. S. Thejaswini, “Privacy-preserving runtime verification,” in <i>Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security</i>, Taipei, Taiwan, 2025, pp. 2774–2787.","chicago":"Henzinger, Thomas A, Mahyar Karimi, and K. S. Thejaswini. “Privacy-Preserving Runtime Verification.” In <i>Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security</i>, 2774–87. Association for Computing Machinery, 2025. <a href=\"https://doi.org/10.1145/3719027.3765137\">https://doi.org/10.1145/3719027.3765137</a>.","short":"T.A. Henzinger, M. Karimi, K.S. Thejaswini, in:, Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security, Association for Computing Machinery, 2025, pp. 2774–2787.","mla":"Henzinger, Thomas A., et al. “Privacy-Preserving Runtime Verification.” <i>Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security</i>, Association for Computing Machinery, 2025, pp. 2774–87, doi:<a href=\"https://doi.org/10.1145/3719027.3765137\">10.1145/3719027.3765137</a>."},"page":"2774-2787","day":"22","ddc":["000"],"publication":"Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security","author":[{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724"},{"orcid":"0009-0005-0820-1696","last_name":"Karimi","first_name":"Mahyar","full_name":"Karimi, Mahyar","id":"6e5417ba-5355-11ee-ae5a-94c2e510b26b"},{"first_name":"K. S.","last_name":"Thejaswini","full_name":"Thejaswini, K. S.","id":"3807fb92-fdc1-11ee-bb4a-b4d8a431c753"}],"title":"Privacy-preserving runtime verification","conference":{"name":"CCS: Conference on Computer and Communications Security","start_date":"2025-10-13","end_date":"2025-10-17","location":"Taipei, Taiwan"},"type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"Yes (via OA deal)","file_date_updated":"2026-01-21T07:34:58Z","OA_place":"publisher","related_material":{"record":[{"relation":"dissertation_contains","id":"21401","status":"public"}]},"oa_version":"Published Version","date_updated":"2026-03-13T13:37:19Z","fulldoi":"https://doi.org/10.1145/3719027.3765137","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"ec_funded":1,"arxiv":1,"scopus_import":"1","corr_author":"1","department":[{"_id":"ToHe"},{"_id":"GradSch"}],"date_published":"2025-11-22T00:00:00Z","acknowledgement":"This work is a part of projects VAMOS that has received fund-ing from the European Research Council (ERC), grant agreementNo 101020093 and the Austrian Science Fund (FWF) SFB projectSpyCoDe F8502.We thank anonymous reviewers for pointing us to related work [ 3] and for their valuable suggestions that improved this paper.","status":"public","language":[{"iso":"eng"}],"year":"2025","abstract":[{"text":"Runtime verification offers scalable solutions to improve the safety and reliability of systems. However, systems that require verification or monitoring by a third party to ensure compliance with a specification might contain sensitive information, causing privacy concerns when usual runtime verification approaches are used. Privacy is compromised if protected information about the system, or sensitive data that is processed by the system, is revealed. In addition, revealing the specification being monitored may undermine the essence of third-party verification.\r\nIn this work, we propose two novel protocols for the privacy-preserving runtime verification of systems against formal sequential specifications. In our first protocol, the monitor verifies whether the system satisfies the specification without learning anything else, though both parties are aware of the specification. Our second protocol ensures that the system remains oblivious to the monitored specification, while the monitor learns only whether the system satisfies the specification and nothing more. Our protocols adapt and improve existing techniques used in cryptography, and more specifically, multi-party computation.\r\nThe sequential specification defines the observation step of the monitor, whose granularity depends on the situation (e.g., banks may be monitored on a daily basis). Our protocols exchange a single message per observation step, after an initialisation phase. This design minimises communication overhead, enabling relatively lightweight privacy-preserving monitoring. We implement our approach for monitoring specifications described by register automata and evaluate it experimentally.","lang":"eng"}],"date_created":"2026-01-20T10:17:10Z","OA_type":"hybrid","publication_identifier":{"isbn":["9798400715259"]},"_id":"21020","month":"11","publisher":"Association for Computing Machinery","file":[{"success":1,"date_created":"2026-01-21T07:34:58Z","creator":"dernst","file_id":"21024","access_level":"open_access","file_name":"2025_CCS_HenzingerT.pdf","relation":"main_file","file_size":1241912,"checksum":"615ffddab6c7285158c2953acec6fa6f","content_type":"application/pdf","date_updated":"2026-01-21T07:34:58Z"}],"external_id":{"arxiv":["2505.09276"]},"publication_status":"published","has_accepted_license":"1"},{"abstract":[{"lang":"eng","text":"Hypertrace logic is a sorted first-order logic with separate sorts for time and execution traces. Its formulas specify hyperproperties, which are properties relating multiple traces. In this work, we extend hypertrace logic by introducing trace quantifiers that range over the set of all possible traces. In this extended logic, formulas can quantify over two kinds of trace variables: constrained trace variables, which range over a fixed set of traces defined by the model, and unconstrained trace variables, which can be assigned to any trace. In comparison, hyperlogics such as HyperLTL have only constrained trace quantifiers. We use hypertrace logic to study how different quantifier patterns affect the decidability of the satisfiability problem. We prove that hypertrace logic without constrained trace quantifiers is equivalent to monadic second-order logic of one successor (S1S), and therefore satisfiable, and that the trace-prefixed fragment (all trace quantifiers precede all time quantifiers) is equivalent to HyperQPTL. Moreover, we show that all hypertrace formulas where the only alternation between constrained trace quantifiers is from an existential to a universal quantifier are equisatisfiable to formulas without constraints on their trace variables and, therefore, decidable as well. Our framework allows us to study also time-prefixed hyperlogics, for which we provide new decidability and undecidability results."}],"date_created":"2026-01-29T15:39:15Z","OA_type":"gold","year":"2025","publication_status":"published","has_accepted_license":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","file":[{"date_created":"2026-02-11T09:33:20Z","success":1,"creator":"dernst","file_id":"21213","access_level":"open_access","file_name":"2025_LIPIcS_Chalupa.pdf","relation":"main_file","checksum":"8188ee5c7b14193d48eeb655e9bbdc47","file_size":933970,"content_type":"application/pdf","date_updated":"2026-02-11T09:33:20Z"}],"external_id":{"arxiv":["2510.12298"]},"_id":"21089","month":"12","arxiv":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"ec_funded":1,"fulldoi":"https://doi.org/10.4230/LIPICS.FSTTCS.2025.20","language":[{"iso":"eng"}],"status":"public","date_published":"2025-12-09T00:00:00Z","acknowledgement":"This work was supported in part by the Austrian Science Fund (FWF) SFB project SpyCoDe 10.55776/F85 and by the ERC Advanced Grant VAMOS 101020093.","scopus_import":"1","corr_author":"1","department":[{"_id":"ToHe"}],"article_processing_charge":"No","author":[{"id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","full_name":"Chalupa, Marek","first_name":"Marek","last_name":"Chalupa"},{"orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A"},{"last_name":"Oliveira da Costa","first_name":"Ana A","id":"8b282559-50b0-11ef-861e-d6ace0d92e9b","full_name":"Oliveira da Costa, Ana A"}],"title":"Flavors of quantifiers in hyperlogics","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","conference":{"name":"FSTTCS: Conference on Foundations of Software Technology and Theoretical Computer Science","start_date":"2025-12-17","end_date":"2025-12-19","location":"Pilani, India"},"volume":360,"publication":"45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science","ddc":["000"],"alternative_title":["LIPIcs"],"oa_version":"Published Version","date_updated":"2026-02-11T09:35:04Z","file_date_updated":"2026-02-11T09:33:20Z","OA_place":"publisher","doi":"10.4230/LIPICS.FSTTCS.2025.20","project":[{"_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e","name":"Interface Theory for Security and Privacy","grant_number":"F8502"},{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"intvolume":"       360","oa":1,"quality_controlled":"1","day":"09","page":"20:1-20:18","citation":{"ieee":"M. Chalupa, T. A. Henzinger, and A. A. Oliveira da Costa, “Flavors of quantifiers in hyperlogics,” in <i>45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>, Pilani, India, 2025, vol. 360, p. 20:1-20:18.","chicago":"Chalupa, Marek, Thomas A Henzinger, and Ana A Oliveira da Costa. “Flavors of Quantifiers in Hyperlogics.” In <i>45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>, 360:20:1-20:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. <a href=\"https://doi.org/10.4230/LIPICS.FSTTCS.2025.20\">https://doi.org/10.4230/LIPICS.FSTTCS.2025.20</a>.","short":"M. Chalupa, T.A. Henzinger, A.A. Oliveira da Costa, in:, 45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025, p. 20:1-20:18.","mla":"Chalupa, Marek, et al. “Flavors of Quantifiers in Hyperlogics.” <i>45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>, vol. 360, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025, p. 20:1-20:18, doi:<a href=\"https://doi.org/10.4230/LIPICS.FSTTCS.2025.20\">10.4230/LIPICS.FSTTCS.2025.20</a>.","ista":"Chalupa M, Henzinger TA, Oliveira da Costa AA. 2025. Flavors of quantifiers in hyperlogics. 45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science. FSTTCS: Conference on Foundations of Software Technology and Theoretical Computer Science, LIPIcs, vol. 360, 20:1-20:18.","apa":"Chalupa, M., Henzinger, T. A., &#38; Oliveira da Costa, A. A. (2025). Flavors of quantifiers in hyperlogics. In <i>45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i> (Vol. 360, p. 20:1-20:18). Pilani, India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPICS.FSTTCS.2025.20\">https://doi.org/10.4230/LIPICS.FSTTCS.2025.20</a>","ama":"Chalupa M, Henzinger TA, Oliveira da Costa AA. Flavors of quantifiers in hyperlogics. In: <i>45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>. Vol 360. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2025:20:1-20:18. doi:<a href=\"https://doi.org/10.4230/LIPICS.FSTTCS.2025.20\">10.4230/LIPICS.FSTTCS.2025.20</a>"}},{"doi":"10.1007/978-3-032-05435-7_4","project":[{"name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2507.11987","open_access":"1"}],"oa":1,"intvolume":"     16087","quality_controlled":"1","day":"13","page":"54-72","citation":{"short":"T.A. Henzinger, K. Kueffner, E. Yu, in:, 25th International Conference on Runtime Verification, Springer Nature, 2025, pp. 54–72.","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>.","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>.","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>","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>","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."},"article_processing_charge":"No","conference":{"name":"RV: Runtime Verification","start_date":"2025-09-15","end_date":"2025-09-19","location":"Graz, Austria"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","author":[{"orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A"},{"first_name":"Konstantin","last_name":"Kueffner","full_name":"Kueffner, Konstantin","id":"8121a2d0-dc85-11ea-9058-af578f3b4515","orcid":"0000-0001-8974-2542"},{"orcid":"0000-0002-4993-773X","full_name":"Yu, Zhengqi","id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342","last_name":"Yu","first_name":"Zhengqi"}],"title":"Formal verification of neural certificates done dynamically","publication":"25th International Conference on Runtime Verification","volume":16087,"date_updated":"2026-02-16T11:53:25Z","oa_version":"Preprint","alternative_title":["LNCS"],"OA_place":"repository","arxiv":1,"ec_funded":1,"fulldoi":"https://doi.org/10.1007/978-3-032-05435-7_4","language":[{"iso":"eng"}],"status":"public","acknowledgement":"This work is supported by the European Research Council under Grant No.: ERC-2020-AdG 101020093.","date_published":"2025-09-13T00:00:00Z","department":[{"_id":"ToHe"}],"corr_author":"1","publication_identifier":{"issn":["0302-9743"],"eisbn":["9783032054357"],"eissn":["1611-3349"]},"OA_type":"green","date_created":"2026-01-29T16:03:01Z","abstract":[{"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.","lang":"eng"}],"year":"2025","publication_status":"published","external_id":{"arxiv":["2507.11987"]},"publisher":"Springer Nature","_id":"21091","month":"09"},{"arxiv":1,"fulldoi":"https://doi.org/10.1007/978-3-032-05435-7_9","ec_funded":1,"status":"public","language":[{"iso":"eng"}],"department":[{"_id":"ToHe"}],"corr_author":"1","date_published":"2025-09-13T00:00:00Z","acknowledgement":"This work is supported by the European Research Council under Grant No.: ERC-2020-AdG 101020093.","publication_identifier":{"issn":["0302-9743"],"eisbn":["9783032054357"],"eissn":["1611-3349"]},"year":"2025","abstract":[{"lang":"eng","text":"Formal verification provides assurances that a probabilistic system satisfies its specification—conditioned on the system model being aligned with reality. We propose alignment monitoring to watch that this assumption is justified. We consider a probabilistic model well aligned if it accurately predicts the behaviour of an uncertain system in advance. An alignment score measures this by quantifying the similarity between the model’s predicted and the system’s (unknown) actual distributions. An alignment monitor observes the system at runtime; at each point in time it uses the current state and the model to predict the next state. After the next state is observed, the monitor updates the verdict, which is a high-probability interval estimate for the true alignment score. We utilize tools from sequential forecasting to construct our alignment monitors. Besides a monitor for measuring the expected alignment score, we introduce a differential alignment monitor, designed for comparing two models, and a weighted alignment monitor, which permits task-specific alignment monitoring. We evaluate our monitors experimentally on the PRISM benchmark suite. They are fast, memory-efficient, and detect misalignment early."}],"date_created":"2026-01-29T16:03:43Z","OA_type":"green","publisher":"Springer Nature","external_id":{"arxiv":["2508.00021"]},"publication_status":"published","_id":"21092","month":"09","project":[{"name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2508.00021","open_access":"1"}],"doi":"10.1007/978-3-032-05435-7_9","quality_controlled":"1","intvolume":"     16087","oa":1,"page":"140-159","day":"13","citation":{"ista":"Henzinger TA, Kueffner K, Singh V, Sun I. 2025. Alignment monitoring. 25th International Conference on Runtime Verification. RV: Runtime Verification, LNCS, vol. 16087, 140–159.","apa":"Henzinger, T. A., Kueffner, K., Singh, V., &#38; Sun, I. (2025). Alignment monitoring. In <i>25th International Conference on Runtime Verification</i> (Vol. 16087, pp. 140–159). Graz, Austria: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-032-05435-7_9\">https://doi.org/10.1007/978-3-032-05435-7_9</a>","ama":"Henzinger TA, Kueffner K, Singh V, Sun I. Alignment monitoring. In: <i>25th International Conference on Runtime Verification</i>. Vol 16087. Springer Nature; 2025:140-159. doi:<a href=\"https://doi.org/10.1007/978-3-032-05435-7_9\">10.1007/978-3-032-05435-7_9</a>","ieee":"T. A. Henzinger, K. Kueffner, V. Singh, and I. Sun, “Alignment monitoring,” in <i>25th International Conference on Runtime Verification</i>, Graz, Austria, 2025, vol. 16087, pp. 140–159.","short":"T.A. Henzinger, K. Kueffner, V. Singh, I. Sun, in:, 25th International Conference on Runtime Verification, Springer Nature, 2025, pp. 140–159.","chicago":"Henzinger, Thomas A, Konstantin Kueffner, Vasu Singh, and I Sun. “Alignment Monitoring.” In <i>25th International Conference on Runtime Verification</i>, 16087:140–59. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-032-05435-7_9\">https://doi.org/10.1007/978-3-032-05435-7_9</a>.","mla":"Henzinger, Thomas A., et al. “Alignment Monitoring.” <i>25th International Conference on Runtime Verification</i>, vol. 16087, Springer Nature, 2025, pp. 140–59, doi:<a href=\"https://doi.org/10.1007/978-3-032-05435-7_9\">10.1007/978-3-032-05435-7_9</a>."},"author":[{"orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A"},{"orcid":"0000-0001-8974-2542","last_name":"Kueffner","first_name":"Konstantin","full_name":"Kueffner, Konstantin","id":"8121a2d0-dc85-11ea-9058-af578f3b4515"},{"full_name":"Singh, Vasu","id":"4DAE2708-F248-11E8-B48F-1D18A9856A87","first_name":"Vasu","last_name":"Singh"},{"full_name":"Sun, I","last_name":"Sun","first_name":"I"}],"title":"Alignment monitoring","conference":{"location":"Graz, Austria","end_date":"2025-09-19","start_date":"2025-09-15","name":"RV: Runtime Verification"},"type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","volume":16087,"publication":"25th International Conference on Runtime Verification","oa_version":"Preprint","date_updated":"2026-02-16T11:56:38Z","alternative_title":["LNCS"],"OA_place":"repository"},{"_id":"21093","month":"09","publisher":"Springer Nature","external_id":{"arxiv":["2508.02301"]},"publication_status":"published","year":"2025","abstract":[{"text":"We propose a monitoring approach for hyperproperties where the system’s observations range over infinite domains. The specifications are given as formulas of symbolic hypernode logic, an extension of earlier versions of hypernode logic that supports events with data. We demonstrate how to translate terms of symbolic hypernode logic into multi-tape symbolic transducers and we present a monitoring algorithm for universally quantified formulas that is based on this translation. We evaluate our approach against the previous approach for monitoring hypernode logic, and we also compare it to other monitors for hyperproperties.","lang":"eng"}],"date_created":"2026-01-29T16:04:31Z","OA_type":"green","publication_identifier":{"issn":["0302-9743"],"eisbn":["9783032054357"],"eissn":["1611-3349"]},"corr_author":"1","department":[{"_id":"ToHe"}],"date_published":"2025-09-13T00:00:00Z","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093 and in part by the FWF-2022-SFB F8502 (SPyCoDe).","status":"public","language":[{"iso":"eng"}],"fulldoi":"https://doi.org/10.1007/978-3-032-05435-7_23","ec_funded":1,"arxiv":1,"OA_place":"repository","alternative_title":["LNCS"],"date_updated":"2026-02-16T11:59:20Z","oa_version":"Preprint","volume":16087,"publication":"25th International Conference on Runtime Verification","author":[{"id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","full_name":"Chalupa, Marek","last_name":"Chalupa","first_name":"Marek"},{"first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724"},{"last_name":"Oliveira da Costa","first_name":"Ana A","full_name":"Oliveira da Costa, Ana A","id":"8b282559-50b0-11ef-861e-d6ace0d92e9b"}],"title":"Monitoring hypernode logic over infinite domains","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"location":"Graz, Austria","end_date":"2025-09-19","start_date":"2025-09-15","name":"RV: Runtime Verification"},"type":"conference","article_processing_charge":"No","citation":{"ista":"Chalupa M, Henzinger TA, Oliveira da Costa AA. 2025. Monitoring hypernode logic over infinite domains. 25th International Conference on Runtime Verification. RV: Runtime Verification, LNCS, vol. 16087, 417–437.","ama":"Chalupa M, Henzinger TA, Oliveira da Costa AA. Monitoring hypernode logic over infinite domains. In: <i>25th International Conference on Runtime Verification</i>. Vol 16087. Springer Nature; 2025:417-437. doi:<a href=\"https://doi.org/10.1007/978-3-032-05435-7_23\">10.1007/978-3-032-05435-7_23</a>","apa":"Chalupa, M., Henzinger, T. A., &#38; Oliveira da Costa, A. A. (2025). Monitoring hypernode logic over infinite domains. In <i>25th International Conference on Runtime Verification</i> (Vol. 16087, pp. 417–437). Graz, Austria: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-032-05435-7_23\">https://doi.org/10.1007/978-3-032-05435-7_23</a>","ieee":"M. Chalupa, T. A. Henzinger, and A. A. Oliveira da Costa, “Monitoring hypernode logic over infinite domains,” in <i>25th International Conference on Runtime Verification</i>, Graz, Austria, 2025, vol. 16087, pp. 417–437.","mla":"Chalupa, Marek, et al. “Monitoring Hypernode Logic over Infinite Domains.” <i>25th International Conference on Runtime Verification</i>, vol. 16087, Springer Nature, 2025, pp. 417–37, doi:<a href=\"https://doi.org/10.1007/978-3-032-05435-7_23\">10.1007/978-3-032-05435-7_23</a>.","chicago":"Chalupa, Marek, Thomas A Henzinger, and Ana A Oliveira da Costa. “Monitoring Hypernode Logic over Infinite Domains.” In <i>25th International Conference on Runtime Verification</i>, 16087:417–37. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-032-05435-7_23\">https://doi.org/10.1007/978-3-032-05435-7_23</a>.","short":"M. Chalupa, T.A. Henzinger, A.A. Oliveira da Costa, in:, 25th International Conference on Runtime Verification, Springer Nature, 2025, pp. 417–437."},"page":"417-437","day":"13","quality_controlled":"1","intvolume":"     16087","oa":1,"project":[{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"},{"name":"Interface Theory for Security and Privacy","grant_number":"F8502","_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e"}],"main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2508.02301","open_access":"1"}],"doi":"10.1007/978-3-032-05435-7_23"},{"publisher":"IEEE","date_updated":"2026-05-18T08:34:15Z","oa_version":"None","publication_status":"published","month":"10","_id":"21885","title":"Neural Certificates","author":[{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724"}],"conference":{"location":"Timisoara, Romania","end_date":"2025-09-25","start_date":"2025-09-22","name":"SYNASC: Symposium on Symbolic and Numeric Algorithms for Scientific Computing"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","publication_identifier":{"eissn":["2470-881X"],"eisbn":["9798331590116"]},"article_processing_charge":"No","year":"2025","abstract":[{"lang":"eng","text":"Symbolic datatypes have proved to be central for automated reasoning about dynamical systems. In its basic form, a symbolic datatype for a class of dynamical systems supports the representation of state and transition sets, boolean operations and emptiness checks on such sets, and the transformation of a state set by a transition set. Successful examples of symbolic datatypes include BDDs and SAT for reasoning about finitestate systems, as well as polyhedra and SMT for reasoning about discrete dynamical systems over multidimensional realvalued state spaces. Most automated verification engines are based on such symbolic datatypes."}],"OA_type":"closed access","publication":"Proceedings of the 27th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing","date_created":"2026-05-17T22:02:11Z","status":"public","language":[{"iso":"eng"}],"day":"01","department":[{"_id":"ToHe"}],"scopus_import":"1","corr_author":"1","date_published":"2025-10-01T00:00:00Z","citation":{"apa":"Henzinger, T. A. (2025). Neural Certificates. In <i>Proceedings of the 27th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing</i>. Timisoara, Romania: IEEE. <a href=\"https://doi.org/10.1109/SYNASC69064.2025.00008\">https://doi.org/10.1109/SYNASC69064.2025.00008</a>","ama":"Henzinger TA. Neural Certificates. In: <i>Proceedings of the 27th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing</i>. IEEE; 2025. doi:<a href=\"https://doi.org/10.1109/SYNASC69064.2025.00008\">10.1109/SYNASC69064.2025.00008</a>","ista":"Henzinger TA. 2025. Neural Certificates. Proceedings of the 27th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing. SYNASC: Symposium on Symbolic and Numeric Algorithms for Scientific Computing.","short":"T.A. Henzinger, in:, Proceedings of the 27th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, IEEE, 2025.","chicago":"Henzinger, Thomas A. “Neural Certificates.” In <i>Proceedings of the 27th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing</i>. IEEE, 2025. <a href=\"https://doi.org/10.1109/SYNASC69064.2025.00008\">https://doi.org/10.1109/SYNASC69064.2025.00008</a>.","mla":"Henzinger, Thomas A. “Neural Certificates.” <i>Proceedings of the 27th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing</i>, IEEE, 2025, doi:<a href=\"https://doi.org/10.1109/SYNASC69064.2025.00008\">10.1109/SYNASC69064.2025.00008</a>.","ieee":"T. A. Henzinger, “Neural Certificates,” in <i>Proceedings of the 27th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing</i>, Timisoara, Romania, 2025."},"doi":"10.1109/SYNASC69064.2025.00008","quality_controlled":"1","fulldoi":"https://doi.org/10.1109/SYNASC69064.2025.00008"},{"fulldoi":"https://doi.org/10.1007/s10703-024-00447-0","ec_funded":1,"PlanS_conform":"1","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"isi":1,"arxiv":1,"department":[{"_id":"ToHe"}],"scopus_import":"1","corr_author":"1","acknowledgement":"This project has received funding from the European Union’s Horizon 2020 research and innovation programme under grant agreement No 956123 and it was funded in part by the Austrian Science Fund (FWF) project W1255-N23, by the Austrian FWF project ZK-35, by the FWF project SpyCoDe 10.55776/F85 and by the ERC-2020-AdG 101020093. This paper extends the text and the results of the manuscript published at FASE 2022 [1].","date_published":"2025-05-01T00:00:00Z","status":"public","language":[{"iso":"eng"}],"year":"2025","date_created":"2024-06-02T22:00:57Z","OA_type":"hybrid","abstract":[{"text":"Contract-based design is a promising methodology for taming the complexity of developing sophisticated systems. A formal contract distinguishes between assumptions, which are constraints that the designer of a component puts on the environments in which the component can be used safely, and guarantees, which are promises that the designer asks from the team that implements the component. A theory of formal contracts can be formalized as an interface theory, which supports the composition and refinement of both assumptions and guarantees. Although there is a rich landscape of contract-based design methods that address functional and extra-functional properties, we present the first interface theory designed to ensure system-wide security properties. Our framework provides a refinement relation and a composition operation that support both incremental design and independent implementability. We develop our theory for both stateless and stateful interfaces. Additionally, we introduce information-flow contracts where assumptions and guarantees are sets of flow relations. We use these contracts to illustrate how to enrich information-flow interfaces with a semantic view. We illustrate the applicability of our framework with two examples inspired by the automotive domain.","lang":"eng"}],"publication_identifier":{"eissn":["1572-8102"],"issn":["0925-9856"]},"_id":"17094","month":"05","external_id":{"isi":["001230084200001"],"arxiv":["2002.06465"]},"file":[{"content_type":"application/pdf","date_updated":"2025-12-30T06:50:12Z","relation":"main_file","checksum":"244a71a916103b8ea08e9d0bab32bcd9","file_size":3860690,"access_level":"open_access","file_id":"20879","file_name":"2025_FormalMethodsSysDesign_Bartocci.pdf","date_created":"2025-12-30T06:50:12Z","success":1,"creator":"dernst"}],"publisher":"Springer Nature","has_accepted_license":"1","publication_status":"published","quality_controlled":"1","oa":1,"intvolume":"        66","project":[{"name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"},{"name":"Interface Theory for Security and Privacy","grant_number":"F8502","_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e"}],"doi":"10.1007/s10703-024-00447-0","citation":{"mla":"Bartocci, Ezio, et al. “Information-Flow Interfaces.” <i>Formal Methods in System Design</i>, vol. 66, Springer Nature, 2025, pp. 3–48, doi:<a href=\"https://doi.org/10.1007/s10703-024-00447-0\">10.1007/s10703-024-00447-0</a>.","chicago":"Bartocci, Ezio, Thomas Ferrere, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira da Costa. “Information-Flow Interfaces.” <i>Formal Methods in System Design</i>. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/s10703-024-00447-0\">https://doi.org/10.1007/s10703-024-00447-0</a>.","short":"E. Bartocci, T. Ferrere, T.A. Henzinger, D. Nickovic, A. Oliveira da Costa, Formal Methods in System Design 66 (2025) 3–48.","ieee":"E. Bartocci, T. Ferrere, T. A. Henzinger, D. Nickovic, and A. Oliveira da Costa, “Information-flow interfaces,” <i>Formal Methods in System Design</i>, vol. 66. Springer Nature, pp. 3–48, 2025.","ama":"Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Oliveira da Costa A. Information-flow interfaces. <i>Formal Methods in System Design</i>. 2025;66:3-48. doi:<a href=\"https://doi.org/10.1007/s10703-024-00447-0\">10.1007/s10703-024-00447-0</a>","apa":"Bartocci, E., Ferrere, T., Henzinger, T. A., Nickovic, D., &#38; Oliveira da Costa, A. (2025). Information-flow interfaces. <i>Formal Methods in System Design</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s10703-024-00447-0\">https://doi.org/10.1007/s10703-024-00447-0</a>","ista":"Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Oliveira da Costa A. 2025. Information-flow interfaces. Formal Methods in System Design. 66, 3–48."},"page":"3-48","article_type":"original","day":"01","ddc":["000"],"publication":"Formal Methods in System Design","volume":66,"type":"journal_article","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"full_name":"Bartocci, Ezio","first_name":"Ezio","last_name":"Bartocci"},{"orcid":"0000-0001-5199-3143","full_name":"Ferrere, Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","last_name":"Ferrere","first_name":"Thomas"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","orcid":"0000-0002-2985-7724"},{"last_name":"Nickovic","first_name":"Dejan","full_name":"Nickovic, Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-8741-5799","first_name":"Ana","last_name":"Oliveira da Costa","id":"f347ec37-6676-11ee-b395-a888cb7b4fb4","full_name":"Oliveira da Costa, Ana"}],"title":"Information-flow interfaces","article_processing_charge":"Yes (via OA deal)","OA_place":"publisher","file_date_updated":"2025-12-30T06:50:12Z","related_material":{"record":[{"status":"public","relation":"shorter_version","id":"11355"}]},"oa_version":"Published Version","date_updated":"2025-12-30T06:50:51Z"},{"publication_identifier":{"eissn":["1091-6490"],"issn":["0027-8424"]},"year":"2025","date_created":"2025-04-06T22:01:32Z","OA_type":"hybrid","abstract":[{"text":"Quantum hardware is inherently fragile and noisy. We find that the accuracy of traditional quantum error correction algorithms can be improved depending on the hardware. Given different hardware specifications, we automatically synthesize hardware-optimal algorithms for parity correction, qubit resetting, and GHZ (Greenberger–Horne–Zeilinger) state preparation. Using stochastic techniques from computer science, our method presents a computational tool to compute exact accuracy guarantees and synthesize optimal algorithms that are often different from traditional ones. We also show that improvements can be gained with respect to the Qiskit transpiler as we compute the hardware-optimal qubit mapping for the GHZ state-preparation problem.","lang":"eng"}],"external_id":{"isi":["001459435600001"],"pmid":["40106357"]},"file":[{"creator":"dernst","success":1,"date_created":"2025-04-07T11:42:22Z","file_name":"2025_PNAS_Muroya.pdf","access_level":"open_access","file_id":"19524","file_size":6805668,"checksum":"83501b8a65ee5fdd3f5604fc28eddc22","relation":"main_file","date_updated":"2025-04-07T11:42:22Z","content_type":"application/pdf"}],"publisher":"National Academy of Sciences","has_accepted_license":"1","publication_status":"published","month":"03","_id":"19499","fulldoi":"https://doi.org/10.1073/pnas.2419273122","pmid":1,"ec_funded":1,"issue":"12","isi":1,"tmp":{"name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","short":"CC BY-NC-ND (4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","image":"/images/cc_by_nc_nd.png"},"status":"public","language":[{"iso":"eng"}],"corr_author":"1","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"scopus_import":"1","acknowledgement":"We thank the reviewers. In particular, they inspired us to analyze the reset and state-preparation problems, to compute optimal qubit mappings, and to apply our method to a quantum error correction scheme that includes both bitflip and phaseflip corrections. We also thank Raimundo Saona and Marek Chalupa for their time spent in insightful discussions. This research was partially supported by the European Research Council CoG 863818 (ForM-SMArt) grant.","article_number":"e2419273122","date_published":"2025-03-25T00:00:00Z","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","type":"journal_article","title":"Hardware-optimal quantum algorithms","author":[{"full_name":"Muroya Lei, Stefanie","id":"a376de31-8972-11ed-ae7b-d0251c13c8ff","last_name":"Muroya Lei","first_name":"Stefanie"},{"orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724"}],"article_processing_charge":"Yes (in subscription journal)","ddc":["000"],"publication":"Proceedings of the National Academy of Sciences","volume":122,"date_updated":"2026-04-28T13:41:14Z","oa_version":"Published Version","OA_place":"publisher","file_date_updated":"2025-04-07T11:42:22Z","related_material":{"link":[{"relation":"software","url":"https://github.com/smml1996/algorithm_synthesis"},{"description":"News on ISTA website","url":"https://ista.ac.at/en/news/hardware-optimal-quantum-algorithms/","relation":"press_release"}]},"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"}],"doi":"10.1073/pnas.2419273122","quality_controlled":"1","oa":1,"intvolume":"       122","article_type":"original","day":"25","citation":{"ama":"Muroya Lei S, Chatterjee K, Henzinger TA. Hardware-optimal quantum algorithms. <i>Proceedings of the National Academy of Sciences</i>. 2025;122(12). doi:<a href=\"https://doi.org/10.1073/pnas.2419273122\">10.1073/pnas.2419273122</a>","apa":"Muroya Lei, S., Chatterjee, K., &#38; Henzinger, T. A. (2025). Hardware-optimal quantum algorithms. <i>Proceedings of the National Academy of Sciences</i>. National Academy of Sciences. <a href=\"https://doi.org/10.1073/pnas.2419273122\">https://doi.org/10.1073/pnas.2419273122</a>","ista":"Muroya Lei S, Chatterjee K, Henzinger TA. 2025. Hardware-optimal quantum algorithms. Proceedings of the National Academy of Sciences. 122(12), e2419273122.","mla":"Muroya Lei, Stefanie, et al. “Hardware-Optimal Quantum Algorithms.” <i>Proceedings of the National Academy of Sciences</i>, vol. 122, no. 12, e2419273122, National Academy of Sciences, 2025, doi:<a href=\"https://doi.org/10.1073/pnas.2419273122\">10.1073/pnas.2419273122</a>.","chicago":"Muroya Lei, Stefanie, Krishnendu Chatterjee, and Thomas A Henzinger. “Hardware-Optimal Quantum Algorithms.” <i>Proceedings of the National Academy of Sciences</i>. National Academy of Sciences, 2025. <a href=\"https://doi.org/10.1073/pnas.2419273122\">https://doi.org/10.1073/pnas.2419273122</a>.","short":"S. Muroya Lei, K. Chatterjee, T.A. Henzinger, Proceedings of the National Academy of Sciences 122 (2025).","ieee":"S. Muroya Lei, K. Chatterjee, and T. A. Henzinger, “Hardware-optimal quantum algorithms,” <i>Proceedings of the National Academy of Sciences</i>, vol. 122, no. 12. National Academy of Sciences, 2025."}},{"day":"11","page":"15659-15668","citation":{"ama":"Cano Cordoba F, Henzinger TA, Könighofer B, Kueffner K, Mallik K. Fairness shields: Safeguarding against biased decision makers. In: <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>. Vol 39. Association for the Advancement of Artificial Intelligence; 2025:15659-15668. doi:<a href=\"https://doi.org/10.1609/aaai.v39i15.33719\">10.1609/aaai.v39i15.33719</a>","apa":"Cano Cordoba, F., Henzinger, T. A., Könighofer, B., Kueffner, K., &#38; Mallik, K. (2025). Fairness shields: Safeguarding against biased decision makers. In <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i> (Vol. 39, pp. 15659–15668). Philadelphia, PA, United States: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v39i15.33719\">https://doi.org/10.1609/aaai.v39i15.33719</a>","ista":"Cano Cordoba F, Henzinger TA, Könighofer B, Kueffner K, Mallik K. 2025. Fairness shields: Safeguarding against biased decision makers. Proceedings of the 39th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 39, 15659–15668.","mla":"Cano Cordoba, Filip, et al. “Fairness Shields: Safeguarding against Biased Decision Makers.” <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, vol. 39, no. 15, Association for the Advancement of Artificial Intelligence, 2025, pp. 15659–68, doi:<a href=\"https://doi.org/10.1609/aaai.v39i15.33719\">10.1609/aaai.v39i15.33719</a>.","chicago":"Cano Cordoba, Filip, Thomas A Henzinger, Bettina Könighofer, Konstantin Kueffner, and Kaushik Mallik. “Fairness Shields: Safeguarding against Biased Decision Makers.” In <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, 39:15659–68. Association for the Advancement of Artificial Intelligence, 2025. <a href=\"https://doi.org/10.1609/aaai.v39i15.33719\">https://doi.org/10.1609/aaai.v39i15.33719</a>.","short":"F. Cano Cordoba, T.A. Henzinger, B. Könighofer, K. Kueffner, K. Mallik, in:, Proceedings of the 39th AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2025, pp. 15659–15668.","ieee":"F. Cano Cordoba, T. A. Henzinger, B. Könighofer, K. Kueffner, and K. Mallik, “Fairness shields: Safeguarding against biased decision makers,” in <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, Philadelphia, PA, United States, 2025, vol. 39, no. 15, pp. 15659–15668."},"doi":"10.1609/aaai.v39i15.33719","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2412.11994"}],"project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"oa":1,"intvolume":"        39","quality_controlled":"1","oa_version":"Preprint","date_updated":"2026-02-16T12:24:30Z","OA_place":"repository","article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","conference":{"end_date":"2025-03-04","location":"Philadelphia, PA, United States","name":"AAAI: Conference on Artificial Intelligence","start_date":"2025-02-25"},"author":[{"orcid":"0000-0002-0783-904X","id":"708cad98-e86a-11ef-8098-bdae2d7c6af1","full_name":"Cano Cordoba, Filip","last_name":"Cano Cordoba","first_name":"Filip"},{"orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A"},{"full_name":"Könighofer, Bettina","last_name":"Könighofer","first_name":"Bettina"},{"id":"8121a2d0-dc85-11ea-9058-af578f3b4515","full_name":"Kueffner, Konstantin","first_name":"Konstantin","last_name":"Kueffner","orcid":"0000-0001-8974-2542"},{"last_name":"Mallik","first_name":"Kaushik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","full_name":"Mallik, Kaushik","orcid":"0000-0001-9864-7475"}],"title":"Fairness shields: Safeguarding against biased decision makers","publication":"Proceedings of the 39th AAAI Conference on Artificial Intelligence","volume":39,"language":[{"iso":"eng"}],"status":"public","acknowledgement":"This work is partly supported by the European Research Council under Grant No.: ERC-2020-AdG 101020093. It is also partially supported by the State Government of Styria, Austria – Department Zukunftsfonds Steiermark.","date_published":"2025-04-11T00:00:00Z","scopus_import":"1","department":[{"_id":"ToHe"}],"corr_author":"1","arxiv":1,"ec_funded":1,"issue":"15","fulldoi":"https://doi.org/10.1609/aaai.v39i15.33719","publication_status":"published","external_id":{"arxiv":["2412.11994"]},"publisher":"Association for the Advancement of Artificial Intelligence","month":"04","_id":"19665","publication_identifier":{"issn":["2159-5399"],"eissn":["2374-3468"]},"date_created":"2025-05-11T22:02:39Z","OA_type":"green","abstract":[{"lang":"eng","text":"As AI-based decision-makers increasingly influence human lives, it is a growing concern that their decisions may be unfair or biased with respect to people's protected attributes, such as gender and race. Most existing bias prevention measures provide probabilistic fairness guarantees in the long run, and it is possible that the decisions are biased on any decision sequence of fixed length. We introduce *fairness shielding*, where a symbolic decision-maker---the fairness shield---continuously monitors the sequence of decisions of another deployed black-box decision-maker, and makes interventions so that a given fairness criterion is met while the total intervention costs are minimized. We present four different algorithms for computing fairness shields, among which one guarantees fairness over fixed horizons, and three guarantee fairness periodically after fixed intervals. Given a distribution over future decisions and their intervention costs, our algorithms solve different instances of bounded-horizon optimal control problems with different levels of computational costs and optimality guarantees. Our empirical evaluation demonstrates the effectiveness of these shields in ensuring fairness while maintaining cost efficiency across various scenarios."}],"year":"2025"},{"page":"26409-26417","day":"11","citation":{"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>","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>","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.","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.","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>.","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>.","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."},"main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2412.12996","open_access":"1"}],"project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"doi":"10.1609/aaai.v39i25.34840","quality_controlled":"1","intvolume":"        39","oa":1,"oa_version":"Preprint","date_updated":"2025-05-12T09:49:25Z","OA_place":"repository","title":"Neural control and certificate repair via runtime monitoring","author":[{"last_name":"Yu","first_name":"Zhengqi","id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342","full_name":"Yu, Zhengqi"},{"full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde","last_name":"Zikelic","orcid":"0000-0002-4681-1699"},{"last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","conference":{"location":"Philadelphia, PA, United States","end_date":"2025-03-04","start_date":"2025-02-25","name":"AAAI: Conference on Artificial Intelligence"},"article_processing_charge":"No","volume":39,"publication":"Proceedings of the 39th AAAI Conference on Artificial Intelligence","status":"public","language":[{"iso":"eng"}],"department":[{"_id":"ToHe"}],"scopus_import":"1","corr_author":"1","date_published":"2025-04-11T00:00:00Z","acknowledgement":"This work was supported in part by the ERC project ERC2020-AdG 101020093","arxiv":1,"fulldoi":"https://doi.org/10.1609/aaai.v39i25.34840","ec_funded":1,"issue":"25","publisher":"Association for the Advancement of Artificial Intelligence","external_id":{"arxiv":["2412.12996"]},"publication_status":"published","_id":"19668","month":"04","publication_identifier":{"issn":["2159-5399"],"eissn":["2374-3468"]},"year":"2025","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"}],"date_created":"2025-05-11T22:02:40Z","OA_type":"green"},{"scopus_import":"1","corr_author":"1","department":[{"_id":"ToHe"}],"acknowledgement":"This work was in part supported by the ERC-2020-AdG 10102009 grant, and in part by the German Research Foundation (DFG) - WE2290/13-2 (Coop2).","date_published":"2025-05-01T00:00:00Z","status":"public","language":[{"iso":"eng"}],"fulldoi":"https://doi.org/10.1007/978-3-031-90660-2_14","ec_funded":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"month":"05","_id":"19739","file":[{"relation":"main_file","file_size":259050,"checksum":"3f604f25dbe37383acb7f8308aad3ca6","content_type":"application/pdf","date_updated":"2025-06-02T07:10:35Z","success":1,"date_created":"2025-06-02T07:10:35Z","creator":"dernst","access_level":"open_access","file_id":"19766","file_name":"2025_TACAS_Chalupa.pdf"}],"publisher":"Springer Nature","has_accepted_license":"1","publication_status":"published","year":"2025","date_created":"2025-05-25T22:17:04Z","OA_type":"hybrid","abstract":[{"text":"Cooperative verification is gaining momentum in recent years. The usual setup in cooperative verification is that a verifier A is run with some pre-defined resources, and if it is not able to verify the program, the verification task is passed to a verifier B together with information learned about the program by verifier A, then the chain can continue to a verifier C, and so on. This scheme is static: tools run one after another in a fixed pre-defined order and fixed parameters and resource limits (the scheme may differ for properties to be analyzed, though).\r\n\r\nBubaak is a program analysis tool that allows to run multiple program verifiers in a dynamically changing combination of parallel and sequential portfolios. Bubaak starts the verification process by invoking an initial set of tasks; every task, when it is done (e.g., because of hitting a time limit or finishing its job), rewrites itself into one or more successor tasks. New tasks can be also spawned upon events generated by other tasks. This all happens dynamically based on the information gathered by finished and running tasks. During their execution, tasks that run in parallel can exchange (partial) verification artifacts, either directly or with Bubaak as an intermediary.","lang":"eng"}],"publication_identifier":{"issn":["0302-9743"],"isbn":["9783031906596"],"eissn":["1611-3349"]},"citation":{"short":"M. Chalupa, C. Richter, in:, 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2025, pp. 212–216.","chicago":"Chalupa, Marek, and Cedric Richter. “BUBAAK: Dynamic Cooperative Verification.” In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 15698:212–16. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-90660-2_14\">https://doi.org/10.1007/978-3-031-90660-2_14</a>.","mla":"Chalupa, Marek, and Cedric Richter. “BUBAAK: Dynamic Cooperative Verification.” <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 15698, Springer Nature, 2025, pp. 212–16, doi:<a href=\"https://doi.org/10.1007/978-3-031-90660-2_14\">10.1007/978-3-031-90660-2_14</a>.","ieee":"M. Chalupa and C. Richter, “BUBAAK: Dynamic cooperative verification,” in <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Hamilton, ON, Canada, 2025, vol. 15698, pp. 212–216.","apa":"Chalupa, M., &#38; Richter, C. (2025). BUBAAK: Dynamic cooperative verification. In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 15698, pp. 212–216). Hamilton, ON, Canada: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-90660-2_14\">https://doi.org/10.1007/978-3-031-90660-2_14</a>","ama":"Chalupa M, Richter C. BUBAAK: Dynamic cooperative verification. In: <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 15698. Springer Nature; 2025:212-216. doi:<a href=\"https://doi.org/10.1007/978-3-031-90660-2_14\">10.1007/978-3-031-90660-2_14</a>","ista":"Chalupa M, Richter C. 2025. BUBAAK: Dynamic cooperative verification. 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 15698, 212–216."},"page":"212-216","day":"01","quality_controlled":"1","oa":1,"intvolume":"     15698","project":[{"name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"doi":"10.1007/978-3-031-90660-2_14","OA_place":"publisher","file_date_updated":"2025-06-02T07:10:35Z","date_updated":"2025-06-02T07:21:41Z","alternative_title":["LNCS"],"oa_version":"Published Version","ddc":["000"],"publication":"31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems","volume":15698,"conference":{"start_date":"2025-05-03","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"Hamilton, ON, Canada","end_date":"2025-05-08"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","title":"BUBAAK: Dynamic cooperative verification","author":[{"id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","full_name":"Chalupa, Marek","first_name":"Marek","last_name":"Chalupa"},{"full_name":"Richter, Cedric","last_name":"Richter","first_name":"Cedric"}],"article_processing_charge":"No"},{"file_date_updated":"2025-06-10T07:07:45Z","OA_place":"publisher","related_material":{"link":[{"relation":"software","url":"https://github.com/jcrozum/biobalm"}],"record":[{"relation":"research_data","id":"19800","status":"public"}]},"oa_version":"Published Version","date_updated":"2025-09-30T12:46:33Z","ddc":["000"],"volume":41,"publication":"Bioinformatics","title":"Mapping the attractor landscape of Boolean networks with biobalm","author":[{"full_name":"Trinh, Van Giang","last_name":"Trinh","first_name":"Van Giang"},{"full_name":"Park, Kyu Hyong","last_name":"Park","first_name":"Kyu Hyong"},{"orcid":"0000-0003-1993-0331","last_name":"Pastva","first_name":"Samuel","full_name":"Pastva, Samuel","id":"07c5ea74-f61c-11ec-a664-aa7c5d957b2b"},{"full_name":"Rozum, Jordan C.","last_name":"Rozum","first_name":"Jordan C."}],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","type":"journal_article","article_processing_charge":"Yes","citation":{"ista":"Trinh VG, Park KH, Pastva S, Rozum JC. 2025. Mapping the attractor landscape of Boolean networks with biobalm. Bioinformatics. 41(5), btaf280.","ama":"Trinh VG, Park KH, Pastva S, Rozum JC. Mapping the attractor landscape of Boolean networks with biobalm. <i>Bioinformatics</i>. 2025;41(5). doi:<a href=\"https://doi.org/10.1093/bioinformatics/btaf280\">10.1093/bioinformatics/btaf280</a>","apa":"Trinh, V. G., Park, K. H., Pastva, S., &#38; Rozum, J. C. (2025). Mapping the attractor landscape of Boolean networks with biobalm. <i>Bioinformatics</i>. Oxford University Press. <a href=\"https://doi.org/10.1093/bioinformatics/btaf280\">https://doi.org/10.1093/bioinformatics/btaf280</a>","ieee":"V. G. Trinh, K. H. Park, S. Pastva, and J. C. Rozum, “Mapping the attractor landscape of Boolean networks with biobalm,” <i>Bioinformatics</i>, vol. 41, no. 5. Oxford University Press, 2025.","mla":"Trinh, Van Giang, et al. “Mapping the Attractor Landscape of Boolean Networks with Biobalm.” <i>Bioinformatics</i>, vol. 41, no. 5, btaf280, Oxford University Press, 2025, doi:<a href=\"https://doi.org/10.1093/bioinformatics/btaf280\">10.1093/bioinformatics/btaf280</a>.","short":"V.G. Trinh, K.H. Park, S. Pastva, J.C. Rozum, Bioinformatics 41 (2025).","chicago":"Trinh, Van Giang, Kyu Hyong Park, Samuel Pastva, and Jordan C. Rozum. “Mapping the Attractor Landscape of Boolean Networks with Biobalm.” <i>Bioinformatics</i>. Oxford University Press, 2025. <a href=\"https://doi.org/10.1093/bioinformatics/btaf280\">https://doi.org/10.1093/bioinformatics/btaf280</a>."},"article_type":"original","day":"01","quality_controlled":"1","intvolume":"        41","oa":1,"project":[{"name":"IST-BRIDGE: International postdoctoral program","grant_number":"101034413","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","call_identifier":"H2020"}],"doi":"10.1093/bioinformatics/btaf280","_id":"19796","month":"05","publisher":"Oxford University Press","file":[{"file_name":"2025_Bioinformatics_Trinh.pdf","access_level":"open_access","file_id":"19801","creator":"dernst","date_created":"2025-06-10T07:07:45Z","success":1,"date_updated":"2025-06-10T07:07:45Z","content_type":"application/pdf","checksum":"fa9d68aa0f5ce37598a623c9be936f09","file_size":2695801,"relation":"main_file"}],"external_id":{"pmid":["40327535"],"isi":["001493400600001"]},"publication_status":"published","has_accepted_license":"1","year":"2025","abstract":[{"text":"Motivation: Boolean networks are popular dynamical models of cellular processes in systems biology. Their attractors model phenotypes that arise from the interplay of key regulatory subcircuits. A succession diagram (SD) describes this interplay in a discrete analog of Waddington’s epigenetic attractor landscape that allows for fast identification of attractors and attractor control strategies. Efficient computational tools for studying SDs are essential for the understanding of Boolean attractor landscapes and connecting them to their biological functions.\r\nResults: We present a new approach to SD construction for asynchronously updated Boolean networks, implemented in the biologist’s Boolean attractor landscape mapper, biobalm. We compare biobalm to similar tools and find a substantial performance increase in SD construction, attractor identification, and attractor control. We perform the most comprehensive comparative analysis to date of the SD structure in experimentally-validated Boolean models of cell processes and random ensembles. We find that random models (including critical Kauffman networks) have relatively small SDs, indicating simple decision structures. In contrast, nonrandom models from the literature are enriched in extremely large SDs, indicating an abundance of decision points and suggesting the presence of complex Waddington landscapes in nature.\r\nAvailability and implementation: The tool biobalm is available online at https://github.com/jcrozum/biobalm. Further data, scripts for testing, analysis, and figure generation are available online at https://github.com/jcrozum/biobalm-analysis and in the reproducibility artefact at https://doi.org/10.5281/zenodo.13854760.","lang":"eng"}],"OA_type":"gold","date_created":"2025-06-08T22:01:22Z","publication_identifier":{"eissn":["1367-4811"]},"corr_author":"1","department":[{"_id":"ToHe"}],"scopus_import":"1","date_published":"2025-05-01T00:00:00Z","article_number":"btaf280","acknowledgement":"V.-G.T. was supported by Institut Carnot STAR, Marseille, France. K.H.P. was supported by NSF grant MCB1715826 to Réka Albert. S.P. has received funding from the European Union’s Horizon 2020 Research and Innovation Programme under the Marie Sklodowska-Curie Grant Agreement No. 101034413. J.C.R. was supported by internal departmental funds provided by Luis M. Rocha. No funding bodies had any role in study design, analysis, decision to publish, or preparation of the article.","status":"public","language":[{"iso":"eng"}],"DOAJ_listed":"1","pmid":1,"fulldoi":"https://doi.org/10.1093/bioinformatics/btaf280","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"isi":1,"issue":"5","ec_funded":1},{"scopus_import":"1","corr_author":"1","department":[{"_id":"ToHe"}],"article_number":"11","acknowledgement":"Ondřej Huvar has been supported by the Czech Science Foundation grant No. GA22-10845S. Samuel Pastva received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Sklodowska-Curie Grant Agreement No. 101034413. Kyu Hyong Park and Réka Albert have been supported by NSF grant MCB 1715826 and ARO grant 79961-SM-MUR. No funding bodies had any role in study design, analysis, decision to publish, or preparation of the manuscript.","date_published":"2025-06-12T00:00:00Z","status":"public","language":[{"iso":"eng"}],"fulldoi":"https://doi.org/10.1007/s00285-025-02235-8","ec_funded":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"isi":1,"arxiv":1,"month":"06","_id":"19854","external_id":{"arxiv":["2410.03976"],"isi":["001507009300001"]},"publisher":"Springer Nature","file":[{"content_type":"application/pdf","date_updated":"2025-06-23T11:10:01Z","relation":"main_file","file_size":1243163,"checksum":"a385ef2662f1d0c3497ed3f2721fe594","file_id":"19871","access_level":"open_access","file_name":"2025_JourMathBiology_Pastva.pdf","success":1,"date_created":"2025-06-23T11:10:01Z","creator":"dernst"}],"has_accepted_license":"1","publication_status":"published","year":"2025","date_created":"2025-06-22T22:02:05Z","OA_type":"hybrid","abstract":[{"lang":"eng","text":"Asynchronous Boolean networks are a type of discrete dynamical system in which each variable can take one of two states, and a single variable state is updated in each time step according to pre-selected rules. Boolean networks are popular in systems biology due to their ability to model long-term biological phenotypes within a qualitative, predictive framework. Boolean networks model phenotypes as attractors, which are closely linked to minimal trap spaces (inescapable hypercubes in the system’s state space). In biological applications, attractors and minimal trap spaces are typically in one-to-one correspondence. However, this correspondence is not guaranteed: motif-avoidant attractors (MAAs) that lie outside minimal trap spaces are possible. MAAs are rare and poorly understood, despite recent efforts. In this contribution to the BMB & JMB Special Collection “Problems, Progress and Perspectives in Mathematical and Computational Biology”, we summarize the current state of knowledge regarding MAAs and present several novel observations regarding their response to node deletion reductions and linear extensions of edges. We conduct large-scale computational studies on an ensemble of 14 000 models derived from published Boolean models of biological systems, and more than 100 million Random Boolean Networks. Our findings quantify the rarity of MAAs; in particular, we only observed MAAs in biological models after applying standard simplification methods, highlighting the role of network reduction in introducing MAAs into the dynamics. We also show that MAAs are fragile to linear extensions: in sparse networks, even a single linear node can disrupt virtually all MAAs. Motivated by this observation, we improve the upper bound on the number of delays needed to disrupt a motif-avoidant attractor."}],"publication_identifier":{"eissn":["1432-1416"],"issn":["0303-6812"]},"citation":{"ieee":"S. Pastva, K. H. Park, O. Huvar, J. C. Rozum, and R. Albert, “An open problem: Why are motif-avoidant attractors so rare in asynchronous Boolean networks?,” <i>Journal of Mathematical Biology</i>, vol. 91. Springer Nature, 2025.","mla":"Pastva, Samuel, et al. “An Open Problem: Why Are Motif-Avoidant Attractors so Rare in Asynchronous Boolean Networks?” <i>Journal of Mathematical Biology</i>, vol. 91, 11, Springer Nature, 2025, doi:<a href=\"https://doi.org/10.1007/s00285-025-02235-8\">10.1007/s00285-025-02235-8</a>.","short":"S. Pastva, K.H. Park, O. Huvar, J.C. Rozum, R. Albert, Journal of Mathematical Biology 91 (2025).","chicago":"Pastva, Samuel, Kyu Hyong Park, Ondřej Huvar, Jordan C. Rozum, and Réka Albert. “An Open Problem: Why Are Motif-Avoidant Attractors so Rare in Asynchronous Boolean Networks?” <i>Journal of Mathematical Biology</i>. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/s00285-025-02235-8\">https://doi.org/10.1007/s00285-025-02235-8</a>.","ista":"Pastva S, Park KH, Huvar O, Rozum JC, Albert R. 2025. An open problem: Why are motif-avoidant attractors so rare in asynchronous Boolean networks? Journal of Mathematical Biology. 91, 11.","ama":"Pastva S, Park KH, Huvar O, Rozum JC, Albert R. An open problem: Why are motif-avoidant attractors so rare in asynchronous Boolean networks? <i>Journal of Mathematical Biology</i>. 2025;91. doi:<a href=\"https://doi.org/10.1007/s00285-025-02235-8\">10.1007/s00285-025-02235-8</a>","apa":"Pastva, S., Park, K. H., Huvar, O., Rozum, J. C., &#38; Albert, R. (2025). An open problem: Why are motif-avoidant attractors so rare in asynchronous Boolean networks? <i>Journal of Mathematical Biology</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s00285-025-02235-8\">https://doi.org/10.1007/s00285-025-02235-8</a>"},"article_type":"original","day":"12","quality_controlled":"1","oa":1,"intvolume":"        91","project":[{"call_identifier":"H2020","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","name":"IST-BRIDGE: International postdoctoral program","grant_number":"101034413"}],"doi":"10.1007/s00285-025-02235-8","OA_place":"publisher","file_date_updated":"2025-06-23T11:10:01Z","date_updated":"2025-09-30T13:36:46Z","oa_version":"Published Version","ddc":["000"],"publication":"Journal of Mathematical Biology","volume":91,"type":"journal_article","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","author":[{"orcid":"0000-0003-1993-0331","full_name":"Pastva, Samuel","id":"07c5ea74-f61c-11ec-a664-aa7c5d957b2b","first_name":"Samuel","last_name":"Pastva"},{"full_name":"Park, Kyu Hyong","first_name":"Kyu Hyong","last_name":"Park"},{"first_name":"Ondřej","last_name":"Huvar","full_name":"Huvar, Ondřej"},{"first_name":"Jordan C.","last_name":"Rozum","full_name":"Rozum, Jordan C."},{"full_name":"Albert, Réka","first_name":"Réka","last_name":"Albert"}],"title":"An open problem: Why are motif-avoidant attractors so rare in asynchronous Boolean networks?","article_processing_charge":"Yes (in subscription journal)"},{"fulldoi":"https://doi.org/10.1109/ICSE55347.2025.00092","isi":1,"ec_funded":1,"status":"public","language":[{"iso":"eng"}],"scopus_import":"1","corr_author":"1","department":[{"_id":"ToHe"}],"date_published":"2025-05-01T00:00:00Z","acknowledgement":"This work is partially supported by the German Research Foundation (DFG) – WE2290/13-2 (Coop2), and in part by the ERC-2020-AdG 101020093.","publication_identifier":{"isbn":["9798331505691"],"eissn":["1558-1225"]},"year":"2025","abstract":[{"lang":"eng","text":"Cooperative software verification divides the task of software verification among several verification tools in order to increase efficiency and effectiveness. The basic approach is to let verifiers work on different parts of a program and at the end join verification results. While this idea is intuitively appealing, cooperative verification is usually hindered by the fact that program decomposition (1) is often static, disregarding strengths and weaknesses of employed verifiers, and (2) often represents the decomposed program parts in a specific proprietary format, thereby making the use of off-the-shelf verifiers in cooperative verification difficult. In this paper, we propose a novel cooperative verification scheme that we call dynamic program splitting (DPS). Splitting decomposes programs into (smaller) programs, and thus directly enables the use of off-the-shelf tools. In DPS, splitting is dynamically applied on demand: Verification starts by giving a verification task (a program plus a correctness specification) to a verifier V1. Whenever V1 finds the current task to be hard to verify, it splits the task (i.e., the program) and restarts verification on subtasks. DPS continues until (1) a violation is found, (2) all subtasks are completed or (3) some user-defined stopping criterion is met. In the latter case, the remaining uncompleted subtasks are merged into a single one and are given to a next verifier V2, repeating the same procedure on the still unverified program parts. This way, the decomposition is steered by what is hard to verify for particular verifiers, leveraging their complementary strengths. We have implemented dynamic program splitting and evaluated it on benchmarks of the annual software verification competition SV-COMP. The evaluation shows that cooperative verification with DPS is able to solve verification tasks that none of the constituent verifiers can solve, without any significant overhead."}],"OA_type":"closed access","date_created":"2025-07-16T11:32:29Z","publisher":"IEEE","external_id":{"isi":["001538318100163"]},"publication_status":"published","_id":"20024","month":"05","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"doi":"10.1109/ICSE55347.2025.00092","quality_controlled":"1","page":"2087-2099","day":"01","citation":{"ieee":"C. Richter, M. Chalupa, M.-C. Jakobs, and H. Wehrheim, “Cooperative software verification via dynamic program splitting,” in <i>47th International Conference on Software Engineering</i>, Ottawa, ON, Canada, 2025, pp. 2087–2099.","short":"C. Richter, M. Chalupa, M.-C. Jakobs, H. Wehrheim, in:, 47th International Conference on Software Engineering, IEEE, 2025, pp. 2087–2099.","chicago":"Richter, Cedric, Marek Chalupa, Marie-Christine Jakobs, and Heike Wehrheim. “Cooperative Software Verification via Dynamic Program Splitting.” In <i>47th International Conference on Software Engineering</i>, 2087–99. IEEE, 2025. <a href=\"https://doi.org/10.1109/ICSE55347.2025.00092\">https://doi.org/10.1109/ICSE55347.2025.00092</a>.","mla":"Richter, Cedric, et al. “Cooperative Software Verification via Dynamic Program Splitting.” <i>47th International Conference on Software Engineering</i>, IEEE, 2025, pp. 2087–99, doi:<a href=\"https://doi.org/10.1109/ICSE55347.2025.00092\">10.1109/ICSE55347.2025.00092</a>.","ista":"Richter C, Chalupa M, Jakobs M-C, Wehrheim H. 2025. Cooperative software verification via dynamic program splitting. 47th International Conference on Software Engineering. ICSE: International Conference on Software Engineering, 2087–2099.","apa":"Richter, C., Chalupa, M., Jakobs, M.-C., &#38; Wehrheim, H. (2025). Cooperative software verification via dynamic program splitting. In <i>47th International Conference on Software Engineering</i> (pp. 2087–2099). Ottawa, ON, Canada: IEEE. <a href=\"https://doi.org/10.1109/ICSE55347.2025.00092\">https://doi.org/10.1109/ICSE55347.2025.00092</a>","ama":"Richter C, Chalupa M, Jakobs M-C, Wehrheim H. Cooperative software verification via dynamic program splitting. In: <i>47th International Conference on Software Engineering</i>. IEEE; 2025:2087-2099. doi:<a href=\"https://doi.org/10.1109/ICSE55347.2025.00092\">10.1109/ICSE55347.2025.00092</a>"},"author":[{"first_name":"Cedric","last_name":"Richter","full_name":"Richter, Cedric"},{"first_name":"Marek","last_name":"Chalupa","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","full_name":"Chalupa, Marek"},{"last_name":"Jakobs","first_name":"Marie-Christine","full_name":"Jakobs, Marie-Christine"},{"first_name":"Heike","last_name":"Wehrheim","full_name":"Wehrheim, Heike"}],"title":"Cooperative software verification via dynamic program splitting","conference":{"start_date":"2025-04-26","name":"ICSE: International Conference on Software Engineering","location":"Ottawa, ON, Canada","end_date":"2025-05-06"},"type":"conference","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","article_processing_charge":"No","publication":"47th International Conference on Software Engineering","oa_version":"None","date_updated":"2025-09-30T14:01:55Z"},{"publication_identifier":{"issn":["0001-5903"],"eissn":["1432-0525"]},"abstract":[{"text":"Enforcement of information-flow policies has been extensively studied by language-based approaches over the past few decades. In this paper, we propose an alternative, novel, general, and effective approach using enforcement of hyperproperties– a powerful formalism for expressing and reasoning about a wide range of information-flow security policies. We study black- vs. gray- vs. white-box enforcement of hyperproperties expressed by nondeterministic finite-word hyperautomata (NFH), where the enforcer has null, some, or complete information about the implementation of the system under scrutiny. Given an NFH, in order to generate a runtime enforcer, we reduce the problem to controller synthesis for hyperproperties and subsequently to the satisfiability problem for quantified Boolean formulas (QBFs). The resulting enforcers are transferable with low-overhead. We conduct a rich set of case studies, including information-flow control for JavaScript code, as well as synthesizing obfuscators for control plants.","lang":"eng"}],"date_created":"2025-08-17T22:01:36Z","OA_type":"hybrid","year":"2025","publication_status":"published","has_accepted_license":"1","publisher":"Springer Nature","file":[{"file_name":"2025_ActaInformatica_Hsu.pdf","file_id":"20267","access_level":"open_access","creator":"dernst","date_created":"2025-09-02T05:53:47Z","success":1,"date_updated":"2025-09-02T05:53:47Z","content_type":"application/pdf","checksum":"90a43350fd4a8c5cb5b1b0e1aea7970d","file_size":6505049,"relation":"main_file"}],"external_id":{"isi":["001546115300001"]},"month":"09","_id":"20186","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"PlanS_conform":"1","isi":1,"issue":"3","fulldoi":"https://doi.org/10.1007/s00236-025-00502-1","language":[{"iso":"eng"}],"status":"public","date_published":"2025-09-01T00:00:00Z","article_number":"30","acknowledgement":"This project was funded in part by the Austrian Science Fund (FWF) SFB project SpyCoDe F8502, Vienna Science and Technology Fund (WWTF) [10.47379/ICT19018] (ProbInG) and WWTF project ICT22-023 (TAIGER), National Science Foundation (NSF) CPS Award 1837680, NSF award ECCS-2144416 and NSF SaTC Award 2245114. Open access funding provided by Institute of Science and Technology (IST Austria).","corr_author":"1","scopus_import":"1","department":[{"_id":"ToHe"}],"article_processing_charge":"Yes (via OA deal)","author":[{"full_name":"Hsu, Tzu Han","first_name":"Tzu Han","last_name":"Hsu"},{"last_name":"Oliveira Da Costa","first_name":"Ana A","id":"8b282559-50b0-11ef-861e-d6ace0d92e9b","full_name":"Oliveira Da Costa, Ana A"},{"full_name":"Wintenberg, Andrew","first_name":"Andrew","last_name":"Wintenberg"},{"last_name":"Bartocci","first_name":"Ezio","full_name":"Bartocci, Ezio"},{"first_name":"Borzoo","last_name":"Bonakdarpour","full_name":"Bonakdarpour, Borzoo"}],"title":"Gray-box runtime enforcement of hyperproperties","type":"journal_article","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","volume":62,"publication":"Acta Informatica","ddc":["000"],"oa_version":"Published Version","date_updated":"2025-09-30T14:20:11Z","file_date_updated":"2025-09-02T05:53:47Z","OA_place":"publisher","doi":"10.1007/s00236-025-00502-1","project":[{"_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e","grant_number":"F8502","name":"Interface Theory for Security and Privacy"}],"intvolume":"        62","oa":1,"quality_controlled":"1","day":"01","article_type":"original","citation":{"mla":"Hsu, Tzu Han, et al. “Gray-Box Runtime Enforcement of Hyperproperties.” <i>Acta Informatica</i>, vol. 62, no. 3, 30, Springer Nature, 2025, doi:<a href=\"https://doi.org/10.1007/s00236-025-00502-1\">10.1007/s00236-025-00502-1</a>.","short":"T.H. Hsu, A.A. Oliveira da Costa, A. Wintenberg, E. Bartocci, B. Bonakdarpour, Acta Informatica 62 (2025).","chicago":"Hsu, Tzu Han, Ana A Oliveira da Costa, Andrew Wintenberg, Ezio Bartocci, and Borzoo Bonakdarpour. “Gray-Box Runtime Enforcement of Hyperproperties.” <i>Acta Informatica</i>. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/s00236-025-00502-1\">https://doi.org/10.1007/s00236-025-00502-1</a>.","ieee":"T. H. Hsu, A. A. Oliveira da Costa, A. Wintenberg, E. Bartocci, and B. Bonakdarpour, “Gray-box runtime enforcement of hyperproperties,” <i>Acta Informatica</i>, vol. 62, no. 3. Springer Nature, 2025.","ama":"Hsu TH, Oliveira da Costa AA, Wintenberg A, Bartocci E, Bonakdarpour B. Gray-box runtime enforcement of hyperproperties. <i>Acta Informatica</i>. 2025;62(3). doi:<a href=\"https://doi.org/10.1007/s00236-025-00502-1\">10.1007/s00236-025-00502-1</a>","apa":"Hsu, T. H., Oliveira da Costa, A. A., Wintenberg, A., Bartocci, E., &#38; Bonakdarpour, B. (2025). Gray-box runtime enforcement of hyperproperties. <i>Acta Informatica</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s00236-025-00502-1\">https://doi.org/10.1007/s00236-025-00502-1</a>","ista":"Hsu TH, Oliveira da Costa AA, Wintenberg A, Bartocci E, Bonakdarpour B. 2025. Gray-box runtime enforcement of hyperproperties. Acta Informatica. 62(3), 30."}},{"project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"doi":"10.1007/978-3-031-98668-0_14","quality_controlled":"1","intvolume":"     15931","oa":1,"page":"281-295","day":"01","citation":{"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.","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>.","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.","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>","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>"},"title":"Introducing certificates to the hardware model checking competition","author":[{"full_name":"Froleyks, Nils","last_name":"Froleyks","first_name":"Nils"},{"id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342","full_name":"Yu, Zhengqi","last_name":"Yu","first_name":"Zhengqi","orcid":"0000-0002-4993-773X"},{"last_name":"Preiner","first_name":"Mathias","full_name":"Preiner, Mathias"},{"full_name":"Biere, Armin","first_name":"Armin","last_name":"Biere"},{"full_name":"Heljanko, Keijo","last_name":"Heljanko","first_name":"Keijo"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"start_date":"2025-07-23","name":"CAV: Computer Aided Verification","location":"Zagreb, Croatia","end_date":"2025-07-25"},"type":"conference","article_processing_charge":"Yes (in subscription journal)","ddc":["000"],"volume":15931,"publication":"37th International Conference on Computer Aided Verification","alternative_title":["LNCS"],"oa_version":"Published Version","date_updated":"2025-12-01T12:34:05Z","file_date_updated":"2025-09-02T05:46:10Z","OA_place":"publisher","fulldoi":"https://doi.org/10.1007/978-3-031-98668-0_14","isi":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"ec_funded":1,"status":"public","language":[{"iso":"eng"}],"scopus_import":"1","department":[{"_id":"ToHe"}],"date_published":"2025-01-01T00:00:00Z","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.","publication_identifier":{"issn":["0302-9743"],"isbn":["9783031986673"],"eissn":["1611-3349"]},"year":"2025","abstract":[{"lang":"eng","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."}],"date_created":"2025-08-17T22:01:36Z","OA_type":"hybrid","file":[{"success":1,"date_created":"2025-09-02T05:46:10Z","creator":"dernst","access_level":"open_access","file_id":"20266","file_name":"2025_CAV_Froleyks.pdf","relation":"main_file","file_size":1078274,"checksum":"15ec1bc9b9409d3b2736f4c9d5f42fd1","content_type":"application/pdf","date_updated":"2025-09-02T05:46:10Z"}],"publisher":"Springer Nature","external_id":{"isi":["001562507100014"]},"publication_status":"published","has_accepted_license":"1","_id":"20189","month":"01"},{"doi":"10.1007/978-3-031-98679-6_2","project":[{"name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"intvolume":"     15932","oa":1,"quality_controlled":"1","day":"22","page":"29-55","citation":{"ieee":"T. A. Henzinger, K. Mallik, P. Sadeghi, and D. Zikelic, “Supermartingale certificates for quantitative omega-regular verification and control,” in <i>37th International Conference on Computer Aided Verification</i>, Zagreb, Croatia, 2025, vol. 15932, pp. 29–55.","chicago":"Henzinger, Thomas A, Kaushik Mallik, Pouya Sadeghi, and Dorde Zikelic. “Supermartingale Certificates for Quantitative Omega-Regular Verification and Control.” In <i>37th International Conference on Computer Aided Verification</i>, 15932:29–55. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-98679-6_2\">https://doi.org/10.1007/978-3-031-98679-6_2</a>.","short":"T.A. Henzinger, K. Mallik, P. Sadeghi, D. Zikelic, in:, 37th International Conference on Computer Aided Verification, Springer Nature, 2025, pp. 29–55.","mla":"Henzinger, Thomas A., et al. “Supermartingale Certificates for Quantitative Omega-Regular Verification and Control.” <i>37th International Conference on Computer Aided Verification</i>, vol. 15932, Springer Nature, 2025, pp. 29–55, doi:<a href=\"https://doi.org/10.1007/978-3-031-98679-6_2\">10.1007/978-3-031-98679-6_2</a>.","ista":"Henzinger TA, Mallik K, Sadeghi P, Zikelic D. 2025. Supermartingale certificates for quantitative omega-regular verification and control. 37th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 15932, 29–55.","apa":"Henzinger, T. A., Mallik, K., Sadeghi, P., &#38; Zikelic, D. (2025). Supermartingale certificates for quantitative omega-regular verification and control. In <i>37th International Conference on Computer Aided Verification</i> (Vol. 15932, pp. 29–55). Zagreb, Croatia: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-98679-6_2\">https://doi.org/10.1007/978-3-031-98679-6_2</a>","ama":"Henzinger TA, Mallik K, Sadeghi P, Zikelic D. Supermartingale certificates for quantitative omega-regular verification and control. In: <i>37th International Conference on Computer Aided Verification</i>. Vol 15932. Springer Nature; 2025:29-55. doi:<a href=\"https://doi.org/10.1007/978-3-031-98679-6_2\">10.1007/978-3-031-98679-6_2</a>"},"article_processing_charge":"Yes (in subscription journal)","author":[{"orcid":"0000-0002-2985-7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0001-9864-7475","full_name":"Mallik, Kaushik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","last_name":"Mallik","first_name":"Kaushik"},{"full_name":"Sadeghi, Pouya","last_name":"Sadeghi","first_name":"Pouya"},{"first_name":"Dorde","last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699"}],"title":"Supermartingale certificates for quantitative omega-regular verification and control","conference":{"name":"CAV: Computer Aided Verification","start_date":"2025-07-23","end_date":"2025-07-25","location":"Zagreb, Croatia"},"type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","volume":15932,"publication":"37th International Conference on Computer Aided Verification","ddc":["000"],"oa_version":"Published Version","alternative_title":["LNCS"],"date_updated":"2025-12-01T12:34:41Z","file_date_updated":"2025-09-02T07:34:33Z","OA_place":"publisher","arxiv":1,"isi":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"ec_funded":1,"fulldoi":"https://doi.org/10.1007/978-3-031-98679-6_2","language":[{"iso":"eng"}],"status":"public","date_published":"2025-07-22T00:00:00Z","acknowledgement":"This work was supported in part by the Singapore Ministry of Education (MOE) Academic Research Fund (AcRF) Tier 1 grant (Project ID:22-SIS-SMU-100) and the ERC project ERC-2020-AdG 101020093.","scopus_import":"1","department":[{"_id":"ToHe"}],"publication_identifier":{"issn":["0302-9743"],"isbn":["9783031986789"],"eissn":["1611-3349"]},"abstract":[{"lang":"eng","text":"We present the first supermartingale certificate for quantitative \r\n-regular properties of discrete-time infinite-state stochastic systems. Our certificate is defined on the product of the stochastic system and a limit-deterministic Büchi automaton that specifies the property of interest; hence we call it a limit-deterministic Büchi supermartingale (LDBSM). Previously known supermartingale certificates applied only to quantitative reachability, safety, or reach-avoid properties, and to qualitative (i.e., probability 1) \r\n-regular properties.We also present fully automated algorithms for the template-based synthesis of LDBSMs, for the case when the stochastic system dynamics and the controller can be represented in terms of polynomial inequalities. Our experiments demonstrate the ability of our method to solve verification and control tasks for stochastic systems that were beyond the reach of previous supermartingale-based approaches."}],"date_created":"2025-08-24T22:01:31Z","OA_type":"hybrid","year":"2025","publication_status":"published","has_accepted_license":"1","publisher":"Springer Nature","file":[{"file_size":884831,"checksum":"beb1e2637de5b2268cc2262119439113","relation":"main_file","date_updated":"2025-09-02T07:34:33Z","content_type":"application/pdf","creator":"dernst","success":1,"date_created":"2025-09-02T07:34:33Z","file_name":"2025_CAV_HenzingerT.pdf","file_id":"20272","access_level":"open_access"}],"external_id":{"isi":["001562506600002"],"arxiv":["2505.18833"]},"month":"07","_id":"20225"},{"project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"}],"doi":"10.4230/LIPIcs.CONCUR.2025.21","quality_controlled":"1","oa":1,"intvolume":"       348","day":"18","citation":{"ieee":"T. A. Henzinger, P. Kebis, N. A. Mazzocchi, and N. E. Sarac, “Quantitative language automata,” in <i>36th International Conference on Concurrency Theory</i>, Aarhus, Denmark, 2025, vol. 348.","chicago":"Henzinger, Thomas A, Pavol Kebis, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Quantitative Language Automata.” In <i>36th International Conference on Concurrency Theory</i>, Vol. 348. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2025.21\">https://doi.org/10.4230/LIPIcs.CONCUR.2025.21</a>.","short":"T.A. Henzinger, P. Kebis, N.A. Mazzocchi, N.E. Sarac, in:, 36th International Conference on Concurrency Theory, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025.","mla":"Henzinger, Thomas A., et al. “Quantitative Language Automata.” <i>36th International Conference on Concurrency Theory</i>, vol. 348, 21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2025.21\">10.4230/LIPIcs.CONCUR.2025.21</a>.","ista":"Henzinger TA, Kebis P, Mazzocchi NA, Sarac NE. 2025. Quantitative language automata. 36th International Conference on Concurrency Theory. CONCUR: Conference on Concurrency Theory, LIPIcs, vol. 348, 21.","apa":"Henzinger, T. A., Kebis, P., Mazzocchi, N. A., &#38; Sarac, N. E. (2025). Quantitative language automata. In <i>36th International Conference on Concurrency Theory</i> (Vol. 348). Aarhus, Denmark: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2025.21\">https://doi.org/10.4230/LIPIcs.CONCUR.2025.21</a>","ama":"Henzinger TA, Kebis P, Mazzocchi NA, Sarac NE. Quantitative language automata. In: <i>36th International Conference on Concurrency Theory</i>. Vol 348. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2025. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2025.21\">10.4230/LIPIcs.CONCUR.2025.21</a>"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","conference":{"end_date":"2025-08-29","location":"Aarhus, Denmark","name":"CONCUR: Conference on Concurrency Theory","start_date":"2025-08-26"},"type":"conference","author":[{"orcid":"0000-0002-2985-7724","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"first_name":"Pavol","last_name":"Kebis","id":"2e0132b3-4e98-11ef-b275-cf7281c2802a","full_name":"Kebis, Pavol"},{"last_name":"Mazzocchi","first_name":"Nicolas Adrien","id":"b26baa86-3308-11ec-87b0-8990f34baa85","full_name":"Mazzocchi, Nicolas Adrien"},{"last_name":"Sarac","first_name":"Naci E","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","full_name":"Sarac, Naci E"}],"title":"Quantitative language automata","article_processing_charge":"No","ddc":["000"],"publication":"36th International Conference on Concurrency Theory","volume":348,"date_updated":"2025-12-01T12:36:52Z","alternative_title":["LIPIcs"],"oa_version":"Published Version","OA_place":"publisher","file_date_updated":"2025-09-03T10:01:53Z","arxiv":1,"fulldoi":"https://doi.org/10.4230/LIPIcs.CONCUR.2025.21","ec_funded":1,"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"isi":1,"status":"public","language":[{"iso":"eng"}],"department":[{"_id":"ToHe"}],"scopus_import":"1","corr_author":"1","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093.","article_number":"21","date_published":"2025-08-18T00:00:00Z","publication_identifier":{"isbn":["9783959773898"],"issn":["1868-8969"]},"year":"2025","date_created":"2025-08-31T22:01:32Z","OA_type":"gold","abstract":[{"text":"A quantitative word automaton (QWA) defines a function from infinite words to values. For example, every infinite run of a limit-average QWA 𝒜 obtains a mean payoff, and every word w ∈ Σ^ω is assigned the maximal mean payoff obtained by nondeterministic runs of 𝒜 over w. We introduce quantitative language automata (QLAs) that define functions from language generators (i.e., implementations) to values, where a language generator can be nonprobabilistic, defining a set of infinite words, or probabilistic, defining a probability measure over infinite words. A QLA consists of a QWA and an aggregator function. For example, given a QWA 𝒜, the infimum aggregator maps each language L ⊆ Σ^ω to the greatest lower bound assigned by 𝒜 to any word in L. For boolean value sets, QWAs define boolean properties of traces, and QLAs define boolean properties of sets of traces, i.e., hyperproperties. For more general value sets, QLAs serve as a specification language for a generalization of hyperproperties, called quantitative hyperproperties. A nonprobabilistic (resp. probabilistic) quantitative hyperproperty assigns a value to each set (resp. distribution) G of traces, e.g., the minimal (resp. expected) average response time exhibited by the traces in G. We give several examples of quantitative hyperproperties and investigate three paradigmatic problems for QLAs: evaluation, nonemptiness, and universality. In the evaluation problem, given a QLA 𝔸 and an implementation G, we ask for the value that 𝔸 assigns to G. In the nonemptiness (resp. universality) problem, given a QLA 𝔸 and a value k, we ask whether 𝔸 assigns at least k to some (resp. every) language. We provide a comprehensive picture of decidability for these problems for QLAs with common aggregators as well as their restrictions to ω-regular languages and trace distributions generated by finite-state Markov chains.","lang":"eng"}],"external_id":{"arxiv":["2506.0515"],"isi":["001570540800021"]},"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","file":[{"date_updated":"2025-09-03T10:01:53Z","content_type":"application/pdf","file_size":1257397,"checksum":"9d4054058757a73477e6015b10ed6996","relation":"main_file","file_name":"2025_CONCUR_HenzingerT.pdf","file_id":"20282","access_level":"open_access","creator":"dernst","success":1,"date_created":"2025-09-03T10:01:53Z"}],"has_accepted_license":"1","publication_status":"published","month":"08","_id":"20253"},{"day":"01","page":"804-816","citation":{"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.","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.","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.","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.","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.","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.","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."},"project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}],"oa":1,"intvolume":"       283","quality_controlled":"1","date_updated":"2025-09-03T10:37:59Z","alternative_title":["PMLR"],"oa_version":"Published Version","OA_place":"publisher","file_date_updated":"2025-09-03T10:32:12Z","article_processing_charge":"No","conference":{"name":"L4DC: Learning for Dynamics & Control","start_date":"2025-06-04","end_date":"2025-06-06","location":"Ann Arbor, MI, United States"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","title":"Predictive monitoring of black-box dynamical systems","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724"},{"full_name":"Kresse, Fabian","id":"faff3c84-23f6-11ef-9085-e5187b51c604","first_name":"Fabian","last_name":"Kresse"},{"last_name":"Mallik","first_name":"Kaushik","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","full_name":"Mallik, Kaushik","orcid":"0000-0001-9864-7475"},{"first_name":"Zhengqi","last_name":"Yu","full_name":"Yu, Zhengqi","id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342"},{"orcid":"0000-0002-4681-1699","first_name":"Dorde","last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","full_name":"Zikelic, Dorde"}],"publication":"7th Annual Learning for Dynamics & Control Conference","volume":283,"ddc":["000"],"language":[{"iso":"eng"}],"status":"public","acknowledgement":"This work was supported in part by the ERC project ERC-2020-AdG 101020093.\r\n","date_published":"2025-06-01T00:00:00Z","corr_author":"1","scopus_import":"1","department":[{"_id":"ToHe"},{"_id":"ChLa"}],"arxiv":1,"ec_funded":1,"has_accepted_license":"1","publication_status":"published","external_id":{"arxiv":["2412.16564"]},"publisher":"ML Research Press","file":[{"checksum":"d5236e561560635f5ae1d17de4903033","file_size":489639,"relation":"main_file","date_updated":"2025-09-03T10:32:12Z","content_type":"application/pdf","creator":"dernst","date_created":"2025-09-03T10:32:12Z","success":1,"file_name":"2025_L4DC_HenzingerT.pdf","file_id":"20283","access_level":"open_access"}],"_id":"20256","month":"06","publication_identifier":{"eissn":["2640-3498"]},"date_created":"2025-08-31T22:01:32Z","OA_type":"gold","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"}],"year":"2025"},{"volume":345,"publication":"50th International Symposium on Mathematical Foundations of Computer Science","ddc":["000"],"article_processing_charge":"Yes","author":[{"last_name":"Brice","first_name":"Léonard","full_name":"Brice, Léonard"},{"orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"last_name":"Thejaswini","first_name":"K. S.","id":"3807fb92-fdc1-11ee-bb4a-b4d8a431c753","full_name":"Thejaswini, K. S."}],"title":"Finding equilibria: Simpler for pessimists, simplest for optimists","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","conference":{"name":"MFCS: Mathematical Foundations of Computer Science","start_date":"2025-08-25","end_date":"2025-08-29","location":"Warsaw, Poland"},"file_date_updated":"2025-09-08T07:11:12Z","OA_place":"publisher","oa_version":"Published Version","date_updated":"2025-09-08T07:15:40Z","alternative_title":["LIPIcs"],"intvolume":"       345","oa":1,"quality_controlled":"1","doi":"10.4230/LIPIcs.MFCS.2025.30","project":[{"name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}],"citation":{"mla":"Brice, Léonard, et al. “Finding Equilibria: Simpler for Pessimists, Simplest for Optimists.” <i>50th International Symposium on Mathematical Foundations of Computer Science</i>, vol. 345, 30, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025, doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2025.30\">10.4230/LIPIcs.MFCS.2025.30</a>.","short":"L. Brice, T.A. Henzinger, K.S. Thejaswini, in:, 50th International Symposium on Mathematical Foundations of Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025.","chicago":"Brice, Léonard, Thomas A Henzinger, and K. S. Thejaswini. “Finding Equilibria: Simpler for Pessimists, Simplest for Optimists.” In <i>50th International Symposium on Mathematical Foundations of Computer Science</i>, Vol. 345. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2025.30\">https://doi.org/10.4230/LIPIcs.MFCS.2025.30</a>.","ieee":"L. Brice, T. A. Henzinger, and K. S. Thejaswini, “Finding equilibria: Simpler for pessimists, simplest for optimists,” in <i>50th International Symposium on Mathematical Foundations of Computer Science</i>, Warsaw, Poland, 2025, vol. 345.","ama":"Brice L, Henzinger TA, Thejaswini KS. Finding equilibria: Simpler for pessimists, simplest for optimists. In: <i>50th International Symposium on Mathematical Foundations of Computer Science</i>. Vol 345. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2025. doi:<a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2025.30\">10.4230/LIPIcs.MFCS.2025.30</a>","apa":"Brice, L., Henzinger, T. A., &#38; Thejaswini, K. S. (2025). Finding equilibria: Simpler for pessimists, simplest for optimists. In <i>50th International Symposium on Mathematical Foundations of Computer Science</i> (Vol. 345). Warsaw, Poland: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.MFCS.2025.30\">https://doi.org/10.4230/LIPIcs.MFCS.2025.30</a>","ista":"Brice L, Henzinger TA, Thejaswini KS. 2025. Finding equilibria: Simpler for pessimists, simplest for optimists. 50th International Symposium on Mathematical Foundations of Computer Science. MFCS: Mathematical Foundations of Computer Science, LIPIcs, vol. 345, 30."},"day":"20","abstract":[{"text":"We consider equilibria in multiplayer stochastic graph games with terminal-node rewards. In such games, Nash equilibria are defined assuming that each player seeks to maximise their expected payoff, ignoring their aversion or tolerance to risk. We therefore study risk-sensitive equilibria (RSEs), where the expected payoff is replaced by a risk measure. A classical risk measure in the literature is the entropic risk measure, where each player has a real valued parameter capturing their risk-averseness. We introduce the extreme risk measure, which corresponds to extreme cases of entropic risk measure, where players are either extreme optimists or extreme pessimists. Under extreme risk measure, every player is an extremist: an extreme optimist perceives their reward as the maximum payoff that can be achieved with positive probability, while an extreme pessimist expects the minimum payoff achievable with positive probability. We argue that the extreme risk measure, especially in multi-player graph based settings, is particularly relevant as they can model several real life instances such as interactions between secure systems and potential security threats, or distributed controls for safety critical systems. We prove that RSEs defined with the extreme risk measure are guaranteed to exist when all rewards are non-negative. Furthermore, we prove that the problem of deciding whether a given game contains an RSE that generates risk measures within specified intervals is decidable and NP-complete for our extreme risk measure, and even PTIME-complete when all players are extreme optimists, while that same problem is undecidable using the entropic risk measure or even the classical expected payoff. This establishes, to our knowledge, the first decidable fragment for equilibria in simple stochastic games without restrictions on strategy types or number of players.","lang":"eng"}],"date_created":"2025-09-07T22:01:32Z","OA_type":"gold","year":"2025","publication_identifier":{"issn":["1868-8969"],"isbn":["9783959773881"]},"month":"08","_id":"20290","publication_status":"published","has_accepted_license":"1","file":[{"date_created":"2025-09-08T07:11:12Z","success":1,"creator":"dernst","access_level":"open_access","file_id":"20306","file_name":"2025_MFCS_Brice.pdf","relation":"main_file","checksum":"9bc6b8e537662d371d2a27444cbc0b75","file_size":1149694,"content_type":"application/pdf","date_updated":"2025-09-08T07:11:12Z"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","external_id":{"arxiv":["2502.0531"]},"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"ec_funded":1,"fulldoi":"https://doi.org/10.4230/LIPIcs.MFCS.2025.30","arxiv":1,"date_published":"2025-08-20T00:00:00Z","acknowledgement":"This work is a part of project VAMOS that has received funding from the European\r\nResearch Council (ERC), grant agreement No 101020093. We thank anonymous reviewers for pointing us to the Hurwicz criterion and to the work of Gallego-Hernández and Mansutti [13]. We thank Marie van den Bogaard for her valuable feedback on the first author’s PhD dissertation, which helped improve the quality of this work. ","article_number":"30","corr_author":"1","department":[{"_id":"ToHe"}],"scopus_import":"1","language":[{"iso":"eng"}],"status":"public"}]