[{"publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783032262196"]},"scopus_import":"1","das_tickbox":"0","ec_funded":1,"article_processing_charge":"No","alternative_title":["LNCS"],"project":[{"name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093"}],"conference":{"location":"Tokyo, Japan","end_date":"2026-05-22","name":"FM: Formal Methods","start_date":"2026-05-18"},"date_created":"2026-06-14T22:01:44Z","year":"2026","file":[{"file_id":"22113","creator":"dernst","success":1,"date_updated":"2026-06-22T08:18:41Z","file_name":"2026_LNCS_Chalupa.pdf","access_level":"open_access","checksum":"7055199ecb985e9e2e272f4988827067","content_type":"application/pdf","file_size":849237,"date_created":"2026-06-22T08:18:41Z","relation":"main_file"}],"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"intvolume":"     16557","_id":"22006","language":[{"iso":"eng"}],"day":"18","keyword":["Signal first-order logic","Robustness-based quantitative semantics","Online runtime monitoring"],"acknowledgement":"We thank the anonymous reviewers for their helpful comments. This work was supported by the European Research Council (ERC) Grants VAMOS (No. 101020093) and HYPER (No. 101055412), and by the Advanced Research and Invention Agency under the Safeguarded AI programme (MSAI-PR01-P047).","has_accepted_license":"1","publication_status":"published","oa":1,"file_date_updated":"2026-06-22T08:18:41Z","volume":16557,"date_updated":"2026-06-22T08:21:09Z","publication":"27th International Symposium on Formal Methods","arxiv":1,"month":"05","quality_controlled":"1","OA_type":"hybrid","page":"214-233","abstract":[{"text":"Runtime monitoring checks, during execution, whether a partial signal produced by a hybrid system satisfies its specification. Signal First-Order Logic (SFO) offers expressive real-time specifications over such signals, but currently comes only with Boolean semantics and has no tool support. We provide the first robustness-based quantitative semantics for SFO, enabling the expression and evaluation of rich real-time properties beyond the scope of existing formalisms such as Signal Temporal Logic. To enable online monitoring, we identify a past-time fragment of SFO and give a pastification procedure that transforms bounded-response SFO formulas into equisatisfiable formulas in this fragment. We then develop an efficient runtime monitoring algorithm for this past-time fragment and evaluate its performance on a set of benchmarks, demonstrating the practicality and effectiveness of our approach. To the best of our knowledge, this is the first publicly available prototype for online quantitative monitoring of full SFO.","lang":"eng"}],"type":"conference","ddc":["000"],"department":[{"_id":"ToHe"}],"citation":{"ama":"Chalupa M, Henzinger TA, Sarac NE, Yu E. Quantitative monitoring of Signal First-Order logic. In: <i>27th International Symposium on Formal Methods</i>. Vol 16557. Springer Nature; 2026:214-233. doi:<a href=\"https://doi.org/10.1007/978-3-032-26220-2_11\">10.1007/978-3-032-26220-2_11</a>","apa":"Chalupa, M., Henzinger, T. A., Sarac, N. E., &#38; Yu, E. (2026). Quantitative monitoring of Signal First-Order logic. In <i>27th International Symposium on Formal Methods</i> (Vol. 16557, pp. 214–233). Tokyo, Japan: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-032-26220-2_11\">https://doi.org/10.1007/978-3-032-26220-2_11</a>","ista":"Chalupa M, Henzinger TA, Sarac NE, Yu E. 2026. Quantitative monitoring of Signal First-Order logic. 27th International Symposium on Formal Methods. FM: Formal Methods, LNCS, vol. 16557, 214–233.","ieee":"M. Chalupa, T. A. Henzinger, N. E. Sarac, and E. Yu, “Quantitative monitoring of Signal First-Order logic,” in <i>27th International Symposium on Formal Methods</i>, Tokyo, Japan, 2026, vol. 16557, pp. 214–233.","chicago":"Chalupa, Marek, Thomas A Henzinger, Naci E Sarac, and Emily Yu. “Quantitative Monitoring of Signal First-Order Logic.” In <i>27th International Symposium on Formal Methods</i>, 16557:214–33. Springer Nature, 2026. <a href=\"https://doi.org/10.1007/978-3-032-26220-2_11\">https://doi.org/10.1007/978-3-032-26220-2_11</a>.","mla":"Chalupa, Marek, et al. “Quantitative Monitoring of Signal First-Order Logic.” <i>27th International Symposium on Formal Methods</i>, vol. 16557, Springer Nature, 2026, pp. 214–33, doi:<a href=\"https://doi.org/10.1007/978-3-032-26220-2_11\">10.1007/978-3-032-26220-2_11</a>.","short":"M. Chalupa, T.A. Henzinger, N.E. Sarac, E. Yu, in:, 27th International Symposium on Formal Methods, Springer Nature, 2026, pp. 214–233."},"publisher":"Springer Nature","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"first_name":"Marek","full_name":"Chalupa, Marek","last_name":"Chalupa","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"},{"id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","last_name":"Sarac","first_name":"Naci E","full_name":"Sarac, Naci E"},{"last_name":"Yu","id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342","orcid":"0000-0002-4993-773X","first_name":"Zhengqi","full_name":"Yu, Zhengqi"}],"doi":"10.1007/978-3-032-26220-2_11","OA_place":"publisher","oa_version":"Published Version","status":"public","external_id":{"arxiv":["2603.00728"]},"date_published":"2026-05-18T00:00:00Z","title":"Quantitative monitoring of Signal First-Order logic"},{"date_created":"2026-01-20T10:08:21Z","year":"2026","tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"file":[{"file_name":"2026_CommACM_Barrett.pdf","file_id":"21028","success":1,"creator":"dernst","date_updated":"2026-01-21T08:52:07Z","date_created":"2026-01-21T08:52:07Z","file_size":2623108,"relation":"main_file","access_level":"open_access","content_type":"application/pdf","checksum":"d909a9091c254b2d18ba014124663f69"}],"corr_author":"1","day":"01","_id":"21012","intvolume":"        69","language":[{"iso":"eng"}],"publication_identifier":{"issn":["0001-0782"],"eissn":["1557-7317"]},"issue":"1","scopus_import":"1","ec_funded":1,"article_processing_charge":"Yes (via OA deal)","project":[{"call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"article_type":"original","OA_type":"hybrid","page":"66-75","ddc":["000"],"department":[{"_id":"ToHe"}],"type":"journal_article","abstract":[{"text":"In certifiable machine learning, AI systems produce not only results but also verifiable certificates that the results can be trusted.","lang":"eng"}],"author":[{"full_name":"Barrett, Clark","first_name":"Clark","last_name":"Barrett"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"},{"last_name":"Seshia","full_name":"Seshia, Sanjit A.","first_name":"Sanjit A."}],"citation":{"chicago":"Barrett, Clark, Thomas A Henzinger, and Sanjit A. Seshia. “Certificates in AI: Learn but Verify.” <i>Communications of the ACM</i>. Association for Computing Machinery, 2026. <a href=\"https://doi.org/10.1145/3737447\">https://doi.org/10.1145/3737447</a>.","mla":"Barrett, Clark, et al. “Certificates in AI: Learn but Verify.” <i>Communications of the ACM</i>, vol. 69, no. 1, Association for Computing Machinery, 2026, pp. 66–75, doi:<a href=\"https://doi.org/10.1145/3737447\">10.1145/3737447</a>.","short":"C. Barrett, T.A. Henzinger, S.A. Seshia, Communications of the ACM 69 (2026) 66–75.","ama":"Barrett C, Henzinger TA, Seshia SA. Certificates in AI: Learn but verify. <i>Communications of the ACM</i>. 2026;69(1):66-75. doi:<a href=\"https://doi.org/10.1145/3737447\">10.1145/3737447</a>","apa":"Barrett, C., Henzinger, T. A., &#38; Seshia, S. A. (2026). Certificates in AI: Learn but verify. <i>Communications of the ACM</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3737447\">https://doi.org/10.1145/3737447</a>","ista":"Barrett C, Henzinger TA, Seshia SA. 2026. Certificates in AI: Learn but verify. Communications of the ACM. 69(1), 66–75.","ieee":"C. Barrett, T. A. Henzinger, and S. A. Seshia, “Certificates in AI: Learn but verify,” <i>Communications of the ACM</i>, vol. 69, no. 1. Association for Computing Machinery, pp. 66–75, 2026."},"publisher":"Association for Computing Machinery","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","OA_place":"publisher","oa_version":"Published Version","doi":"10.1145/3737447","status":"public","title":"Certificates in AI: Learn but verify","date_published":"2026-01-01T00:00:00Z","PlanS_conform":"1","has_accepted_license":"1","acknowledgement":"T.A.H. thanks Đorde Žikelic for many stimulating discussions about CML. This work was supported in part by NSFCPS Frontier Grant 1545126, by a BAIR Commons project, by the Berkeley iCy-Phy Center, by the Stanford Center for Automated Reasoning, and by the ERC Advanced Grant 101020093.","publication_status":"published","file_date_updated":"2026-01-21T08:52:07Z","oa":1,"volume":69,"date_updated":"2026-01-21T08:55:24Z","publication":"Communications of the ACM","quality_controlled":"1","month":"01"},{"keyword":["Privacy-preserving verification","Runtime verification","Monitoring","Reactive functionalities","Cryptographic protocols"],"day":"05","language":[{"iso":"eng"}],"_id":"21401","file":[{"date_updated":"2026-03-10T15:20:09Z","file_id":"21404","creator":"mkarimi","file_name":"2026_Karimi_Mahyar_Thesis.pdf","access_level":"open_access","checksum":"3f49f05c9d123e14d7adb73d3bc50fe2","content_type":"application/pdf","relation":"main_file","file_size":766048,"date_created":"2026-03-06T14:06:25Z"},{"file_name":"2026_Karimi_Mahyar_Thesis_src.zip","date_updated":"2026-03-06T14:06:25Z","creator":"mkarimi","file_id":"21405","relation":"source_file","date_created":"2026-03-06T14:06:25Z","file_size":1243394,"checksum":"8fb9db4b4187e26443369a993427a5ff","content_type":"application/zip","access_level":"closed"}],"corr_author":"1","related_material":{"record":[{"relation":"part_of_dissertation","status":"public","id":"21020"}]},"year":"2026","date_created":"2026-03-05T15:20:47Z","article_processing_charge":"No","project":[{"name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093"},{"_id":"34a4ce89-11ca-11ed-8bc3-8cc37fb6e11f","grant_number":"F8512","name":"Security and Privacy by Design for Complex Systems"}],"alternative_title":["ISTA Master’s Thesis"],"publication_identifier":{"issn":["2791-4585"]},"ec_funded":1,"oa_version":"Published Version","OA_place":"repository","doi":"10.15479/AT-ISTA-21401","author":[{"orcid":"0009-0005-0820-1696","id":"6e5417ba-5355-11ee-ae5a-94c2e510b26b","last_name":"Karimi","full_name":"Karimi, Mahyar","first_name":"Mahyar"}],"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","citation":{"short":"M. Karimi, Privacy-Preserving Runtime Verification, Institute of Science and Technology Austria, 2026.","mla":"Karimi, Mahyar. <i>Privacy-Preserving Runtime Verification</i>. Institute of Science and Technology Austria, 2026, doi:<a href=\"https://doi.org/10.15479/AT-ISTA-21401\">10.15479/AT-ISTA-21401</a>.","chicago":"Karimi, Mahyar. “Privacy-Preserving Runtime Verification.” Institute of Science and Technology Austria, 2026. <a href=\"https://doi.org/10.15479/AT-ISTA-21401\">https://doi.org/10.15479/AT-ISTA-21401</a>.","ista":"Karimi M. 2026. Privacy-preserving runtime verification. Institute of Science and Technology Austria.","apa":"Karimi, M. (2026). <i>Privacy-preserving runtime verification</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT-ISTA-21401\">https://doi.org/10.15479/AT-ISTA-21401</a>","ieee":"M. Karimi, “Privacy-preserving runtime verification,” Institute of Science and Technology Austria, 2026.","ama":"Karimi M. Privacy-preserving runtime verification. 2026. doi:<a href=\"https://doi.org/10.15479/AT-ISTA-21401\">10.15479/AT-ISTA-21401</a>"},"publisher":"Institute of Science and Technology Austria","title":"Privacy-preserving runtime verification","date_published":"2026-03-05T00:00:00Z","status":"public","page":"60","supervisor":[{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724"}],"department":[{"_id":"GradSch"},{"_id":"ToHe"}],"ddc":["000"],"type":"dissertation","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\n\r\nIn this thesis, we propose a protocol for privacy-preserving runtime verification of systems against formal sequential specifications. We develop the protocol in two steps. In the first step, the monitor verifies whether the system satisfies the specification without learning anything else, though both parties are aware of the specification. In the second step, we extend the protocol to ensure that the system remains oblivious to the monitored specification, while the monitor learns only whether the system satisfies the specification and nothing more. Our protocol adapts and improves existing techniques used in cryptography, and more specifically, multi-party computation.\r\n\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 protocol exchanges a single message per observation step, after an initialization phase. This design minimizes communication overhead, enabling relatively lightweight privacy-preserving monitoring. We implement our approach for monitoring specifications described by register automata and evaluate it experimentally.\r\n","lang":"eng"}],"date_updated":"2026-03-13T13:37:20Z","month":"03","has_accepted_license":"1","acknowledgement":"This work is part of the project VAMOS, which has received funding from the European\r\nResearch Council (ERC) under grant agreement No. 101020093, and the Austrian Science\r\nFund (FWF) SFB project SpyCoDe F8502.\r\n","file_date_updated":"2026-03-10T15:20:09Z","degree_awarded":"MS","oa":1,"publication_status":"published"},{"doi":"10.5220/0014483200004052","oa_version":"Accepted Version","OA_place":"repository","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"chicago":"Cano Cordoba, Filip. “Explaining Decisions One Conversation at a Time: Opportunities and Risks of LLMs as Explainability Assistants.” In <i>Proceedings of the 18th International Conference on Agents and Artificial Intelligence</i>, 5:4689–96. Science and Technology Publications, 2026. <a href=\"https://doi.org/10.5220/0014483200004052\">https://doi.org/10.5220/0014483200004052</a>.","short":"F. Cano Cordoba, in:, Proceedings of the 18th International Conference on Agents and Artificial Intelligence, Science and Technology Publications, 2026, pp. 4689–4696.","mla":"Cano Cordoba, Filip. “Explaining Decisions One Conversation at a Time: Opportunities and Risks of LLMs as Explainability Assistants.” <i>Proceedings of the 18th International Conference on Agents and Artificial Intelligence</i>, vol. 5, Science and Technology Publications, 2026, pp. 4689–96, doi:<a href=\"https://doi.org/10.5220/0014483200004052\">10.5220/0014483200004052</a>.","ama":"Cano Cordoba F. Explaining decisions one conversation at a time: Opportunities and risks of LLMs as explainability assistants. In: <i>Proceedings of the 18th International Conference on Agents and Artificial Intelligence</i>. Vol 5. Science and Technology Publications; 2026:4689-4696. doi:<a href=\"https://doi.org/10.5220/0014483200004052\">10.5220/0014483200004052</a>","ieee":"F. Cano Cordoba, “Explaining decisions one conversation at a time: Opportunities and risks of LLMs as explainability assistants,” in <i>Proceedings of the 18th International Conference on Agents and Artificial Intelligence</i>, Marbella, Spain, 2026, vol. 5, pp. 4689–4696.","ista":"Cano Cordoba F. 2026. Explaining decisions one conversation at a time: Opportunities and risks of LLMs as explainability assistants. Proceedings of the 18th International Conference on Agents and Artificial Intelligence. ICAART: International Conference on Agents and Artificial Intelligence vol. 5, 4689–4696.","apa":"Cano Cordoba, F. (2026). Explaining decisions one conversation at a time: Opportunities and risks of LLMs as explainability assistants. In <i>Proceedings of the 18th International Conference on Agents and Artificial Intelligence</i> (Vol. 5, pp. 4689–4696). Marbella, Spain: Science and Technology Publications. <a href=\"https://doi.org/10.5220/0014483200004052\">https://doi.org/10.5220/0014483200004052</a>"},"publisher":"Science and Technology Publications","author":[{"orcid":"0000-0002-0783-904X","id":"708cad98-e86a-11ef-8098-bdae2d7c6af1","last_name":"Cano Cordoba","full_name":"Cano Cordoba, Filip","first_name":"Filip"}],"title":"Explaining decisions one conversation at a time: Opportunities and risks of LLMs as explainability assistants","date_published":"2026-04-01T00:00:00Z","researchdata_availability":"no","status":"public","page":"4689-4696","OA_type":"green","abstract":[{"text":"Modern AI systems increasingly rely on opaque, highly complex models whose inner workings remain inaccessible even to experts. This opacity creates challenges for trust, accountability, and compliance with\r\nemerging regulatory expectations such as the “right to an explanation”. While traditional explainability methods—feature attributions, counterfactuals, surrogate models—and interpretable model classes provide valuable insights for engineers, they often fall short of delivering the contextual, conversational explanations that\r\nreal users expect. Large Language Models (LLMs) offer a promising new avenue for explanation due to their\r\nability to engage interactively, adapt to user needs, and translate technical outputs into more accessible reasoning. However, their tendencies toward hallucination, conflict avoidance, and oversimplification introduce\r\nserious risks when used as explanatory agents. This paper analyzes these opportunities and limitations, examines verification strategies for ensuring explanation fidelity, and situates LLM-generated explanations within\r\nbroader concerns about public trust. The paper concludes by outlining best practices and future research directions for building robust, verifiable, and human-aligned explanation systems.","lang":"eng"}],"type":"conference","department":[{"_id":"ToHe"}],"date_updated":"2026-06-24T08:37:00Z","volume":5,"month":"04","quality_controlled":"1","publication":"Proceedings of the 18th International Conference on Agents and Artificial Intelligence","acknowledgement":"This work has been supported by the European Research Council under Grant No.: ERC-2020-AdG\r\n101020093. LLM–based tools have been used as\r\nwriting assistance to help improve presentation.\r\n","oa":1,"supplementarymaterial":"no","publication_status":"published","_id":"22103","intvolume":"         5","language":[{"iso":"eng"}],"keyword":["Explainable AI","Large Language Models","Trust in AI"],"day":"01","corr_author":"1","main_file_link":[{"open_access":"1","url":"https://filipcano.org/files/icaart26llm.pdf"}],"conference":{"start_date":"2026-03-05","name":"ICAART: International Conference on Agents and Artificial Intelligence","end_date":"2026-03-08","location":"Marbella, Spain"},"year":"2026","date_created":"2026-06-21T22:03:00Z","article_processing_charge":"No","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020"}],"scopus_import":"1","publication_identifier":{"eissn":["2184-433X"],"isbn":["9789897587962"],"issn":["2184-3589"]},"ec_funded":1,"das_tickbox":"0"},{"file":[{"file_name":"2026_ACMFACCT_Cano.pdf","date_updated":"2026-07-16T09:23:15Z","creator":"dernst","file_id":"22348","success":1,"relation":"main_file","file_size":3129128,"date_created":"2026-07-16T09:23:15Z","checksum":"21e648ea3b529f0df7545ad4b31b0ef4","content_type":"application/pdf","access_level":"open_access"}],"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"corr_author":"1","day":"01","_id":"22321","language":[{"iso":"eng"}],"date_created":"2026-07-14T05:32:45Z","year":"2026","conference":{"start_date":"2026-06-25","name":"FAccT: Conference on Fairness, Accountability and Transparency","location":"Montreal, Canada","end_date":"2026-06-28"},"project":[{"name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093"}],"article_processing_charge":"Yes","das_tickbox":"0","ec_funded":1,"scopus_import":"1","researchdata_availability":"no","status":"public","date_published":"2026-07-01T00:00:00Z","title":"Energy shields for fairness","external_id":{"arxiv":["2605.24926"]},"author":[{"id":"708cad98-e86a-11ef-8098-bdae2d7c6af1","last_name":"Cano Cordoba","orcid":"0000-0002-0783-904X","first_name":"Filip","full_name":"Cano Cordoba, Filip"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger"},{"first_name":"Konstantin","full_name":"Kueffner, Konstantin","orcid":"0000-0001-8974-2542","id":"8121a2d0-dc85-11ea-9058-af578f3b4515","last_name":"Kueffner"}],"publisher":"Association for Computing Machinery","citation":{"apa":"Cano Cordoba, F., Henzinger, T. A., &#38; Kueffner, K. (2026). Energy shields for fairness. In <i>Proceedings of the 2026 ACM Conference on Fairness, Accountability, and Transparency</i> (pp. 4243–4275). Montreal, Canada: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3805689.3806807\">https://doi.org/10.1145/3805689.3806807</a>","ista":"Cano Cordoba F, Henzinger TA, Kueffner K. 2026. Energy shields for fairness. Proceedings of the 2026 ACM Conference on Fairness, Accountability, and Transparency. FAccT: Conference on Fairness, Accountability and Transparency, 4243–4275.","ieee":"F. Cano Cordoba, T. A. Henzinger, and K. Kueffner, “Energy shields for fairness,” in <i>Proceedings of the 2026 ACM Conference on Fairness, Accountability, and Transparency</i>, Montreal, Canada, 2026, pp. 4243–4275.","ama":"Cano Cordoba F, Henzinger TA, Kueffner K. Energy shields for fairness. In: <i>Proceedings of the 2026 ACM Conference on Fairness, Accountability, and Transparency</i>. Association for Computing Machinery; 2026:4243-4275. doi:<a href=\"https://doi.org/10.1145/3805689.3806807\">10.1145/3805689.3806807</a>","mla":"Cano Cordoba, Filip, et al. “Energy Shields for Fairness.” <i>Proceedings of the 2026 ACM Conference on Fairness, Accountability, and Transparency</i>, Association for Computing Machinery, 2026, pp. 4243–75, doi:<a href=\"https://doi.org/10.1145/3805689.3806807\">10.1145/3805689.3806807</a>.","short":"F. Cano Cordoba, T.A. Henzinger, K. Kueffner, in:, Proceedings of the 2026 ACM Conference on Fairness, Accountability, and Transparency, Association for Computing Machinery, 2026, pp. 4243–4275.","chicago":"Cano Cordoba, Filip, Thomas A Henzinger, and Konstantin Kueffner. “Energy Shields for Fairness.” In <i>Proceedings of the 2026 ACM Conference on Fairness, Accountability, and Transparency</i>, 4243–75. Association for Computing Machinery, 2026. <a href=\"https://doi.org/10.1145/3805689.3806807\">https://doi.org/10.1145/3805689.3806807</a>."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","OA_place":"publisher","oa_version":"Published Version","doi":"10.1145/3805689.3806807","ddc":["000"],"department":[{"_id":"ToHe"}],"type":"conference","abstract":[{"text":"Runtime fairness is not a one-time constraint but a dynamic property evaluated over a sequence of decisions. To ensure fairness at runtime, it is necessary to account for past decisions, information neglected by conventional, static classifiers. Traditional fairness shields enforce runtime fairness abruptly, by intervening deterministically whenever a sequence of decisions violates the target for a running fairness measure. This motivates our main conceptual contribution: energy shields. An energy shield is a novel, lightweight, adaptive controller that monitors a sequence of decisions and intervenes probabilistically to ensure runtime fairness smoothly, by utilizing physics-inspired energy functions to nudge the sequence toward fairness: the more unfair the decisions, the stronger the nudging force becomes. This makes energy shields the first fairness shields to provide both short-term safety and long-term liveness guarantees. Safety ensures that the running fairness measure stays within a running target interval with high probability, and liveness ensures that the limit of the fairness measure lies within the limit target interval. Intuitively, the short-term specifies the tolerated fairness values and the long-term specifies the desired fairness values. We also provide a synthesis procedure for constructing the least intrusive energy shield for a given target specification, and demonstrate its efficiency experimentally. We evaluate our energy shields against existing fairness shields through the lens of short- and long-term fairness.","lang":"eng"}],"OA_type":"gold","page":"4243 - 4275","publication":"Proceedings of the 2026 ACM Conference on Fairness, Accountability, and Transparency","quality_controlled":"1","month":"07","arxiv":1,"date_updated":"2026-07-22T06:15:56Z","publication_status":"published","file_date_updated":"2026-07-16T09:23:15Z","supplementarymaterial":"yes","oa":1,"acknowledgement":"This work has been supported by the European Research Council under Grant No.: ERC-2020-AdG 101020093.","has_accepted_license":"1"},{"status":"public","researchdata_availability":"no","external_id":{"arxiv":["2601.18303"]},"title":"Dicey games: Shared sources of randomness in distributed systems","date_published":"2026-07-09T00:00:00Z","article_number":"23:1-23:26","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","citation":{"ama":"Brice LJ, Henzinger TA, Thejaswini KS. Dicey games: Shared sources of randomness in distributed systems. In: <i>41st Annual Symposium on Logic in Computer Science</i>. Vol 380. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2026. doi:<a href=\"https://doi.org/10.4230/LIPIcs.LICS.2026.23\">10.4230/LIPIcs.LICS.2026.23</a>","ieee":"L. J. Brice, T. A. Henzinger, and K. S. Thejaswini, “Dicey games: Shared sources of randomness in distributed systems,” in <i>41st Annual Symposium on Logic in Computer Science</i>, Lisbon, Portugal, 2026, vol. 380.","ista":"Brice LJ, Henzinger TA, Thejaswini KS. 2026. Dicey games: Shared sources of randomness in distributed systems. 41st Annual Symposium on Logic in Computer Science. LICS: Logic in Computer Science, LIPIcs, vol. 380, 23:1-23:26.","apa":"Brice, L. J., Henzinger, T. A., &#38; Thejaswini, K. S. (2026). Dicey games: Shared sources of randomness in distributed systems. In <i>41st Annual Symposium on Logic in Computer Science</i> (Vol. 380). Lisbon, Portugal: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.LICS.2026.23\">https://doi.org/10.4230/LIPIcs.LICS.2026.23</a>","chicago":"Brice, Leonard J, Thomas A Henzinger, and K. S. Thejaswini. “Dicey Games: Shared Sources of Randomness in Distributed Systems.” In <i>41st Annual Symposium on Logic in Computer Science</i>, Vol. 380. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026. <a href=\"https://doi.org/10.4230/LIPIcs.LICS.2026.23\">https://doi.org/10.4230/LIPIcs.LICS.2026.23</a>.","short":"L.J. Brice, T.A. Henzinger, K.S. Thejaswini, in:, 41st Annual Symposium on Logic in Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026.","mla":"Brice, Leonard J., et al. “Dicey Games: Shared Sources of Randomness in Distributed Systems.” <i>41st Annual Symposium on Logic in Computer Science</i>, vol. 380, 23:1-23:26, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2026, doi:<a href=\"https://doi.org/10.4230/LIPIcs.LICS.2026.23\">10.4230/LIPIcs.LICS.2026.23</a>."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"full_name":"Brice, Leonard J","first_name":"Leonard J","last_name":"Brice","id":"ce3b3409-db6c-11f0-aa64-ad678f7fd937"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"full_name":"Thejaswini, K. S.","first_name":"K. S.","last_name":"Thejaswini"}],"doi":"10.4230/LIPIcs.LICS.2026.23","OA_place":"publisher","oa_version":"Published Version","abstract":[{"text":"Consider a 4-player version of Matching Pennies where a team of three players competes against the Devil. Each player simultaneously says \"Heads\" or \"Tails\". The team wins if all four choices match; otherwise the Devil wins. If all team players randomise independently, they win with probability 1/8; if all players share a common source of randomness, they win with probability 1/2. What happens when each pair of team players shares a source of randomness? Can the team do better than win with probability 1/4? The surprising (and nontrivial) answer is yes!\r\nWe introduce Dicey Games, a formal framework motivated by the study of distributed systems with shared sources of randomness (of which the above example is a specific instance). We characterise the existence, representation and computational complexity of optimal strategies in Dicey Games, and we study the problem of allocating limited sources of randomness optimally within a team.","lang":"eng"}],"type":"conference","department":[{"_id":"ToHe"}],"ddc":["000"],"OA_type":"gold","publication":"41st Annual Symposium on Logic in Computer Science","arxiv":1,"month":"07","quality_controlled":"1","volume":380,"date_updated":"2026-08-03T07:03:28Z","publication_status":"published","oa":1,"file_date_updated":"2026-08-03T07:02:30Z","supplementarymaterial":"no","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093 (VAMOS).\r\nLéonard Brice: Part of this work was realised when this author was an FNRS aspirant at Université libre de Bruxelles.\r\nK. S. Thejaswini: Part of this work was realised when this author was a post-doctoral researcher at IST Austria.\r\nAcknowledgements We thank all our colleagues who took the time to hear our puzzle and wasted several hours of their research time in pursuit of the optimal bounds for the 3-player matching.\r\npennies problem.\r\n","has_accepted_license":"1","corr_author":"1","tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"file":[{"date_updated":"2026-08-03T07:02:30Z","file_id":"22625","success":1,"creator":"dernst","file_name":"2026_LIPICSLICS_Brice.pdf","checksum":"5d0ff4d267565188a8b4c7502e1bd243","content_type":"application/pdf","access_level":"open_access","relation":"main_file","date_created":"2026-08-03T07:02:30Z","file_size":919708}],"language":[{"iso":"eng"}],"_id":"22617","intvolume":"       380","day":"09","keyword":["Concurrent games","Shared randomness","Topology","Algebraic Geometry"],"date_created":"2026-08-02T22:01:52Z","year":"2026","conference":{"location":"Lisbon, Portugal","end_date":"2026-07-23","name":"LICS: Logic in Computer Science","start_date":"2026-07-20"},"alternative_title":["LIPIcs"],"project":[{"name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"article_processing_charge":"No","das_tickbox":"0","ec_funded":1,"publication_identifier":{"isbn":["9783959774345"],"issn":["1868-8969"]},"scopus_import":"1"},{"publication_identifier":{"isbn":["9783032325181"],"issn":["0302-9743"],"eissn":["1611-3349"]},"scopus_import":"1","ec_funded":1,"das_tickbox":"1","article_processing_charge":"Yes (in subscription journal)","project":[{"name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093"}],"conference":{"name":"CAV: Computer Aided Verification","start_date":"2026-07-26","end_date":"2026-07-29","location":"Lisbon, Portugal"},"date_created":"2026-08-16T22:01:44Z","year":"2026","file":[{"date_created":"2026-08-18T06:53:22Z","file_size":1902192,"relation":"main_file","access_level":"open_access","checksum":"10ded8a3ab9ed34c9e4794c0b277622c","content_type":"application/pdf","file_name":"2026_LNCS_Brice.pdf","file_id":"22724","success":1,"creator":"dernst","date_updated":"2026-08-18T06:53:22Z"}],"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"_id":"22717","language":[{"iso":"eng"}],"intvolume":"     16682","day":"24","acknowledgement":"This work is a part of project VAMOS that has received funding from the European Research Council (ERC), grant agreement No 101020093. Part of this work was realised when the first author was an FNRS aspirant at Université libre de Bruxelles.","has_accepted_license":"1","publication_status":"published","oa":1,"supplementarymaterial":"no","file_date_updated":"2026-08-18T06:53:22Z","volume":16682,"date_updated":"2026-08-18T06:55:38Z","publication":"38th International Conference on Computer Aided Verification","arxiv":1,"quality_controlled":"1","month":"07","dataavailabilitystatement":"The artifact can be accessed at the link: https://doi. org/10.5281/zenodo.19680359.\r\nThe source code is available at:https://github.com/alipashamontaseri/Team-Concurrent-Game.","page":"215-236","OA_type":"hybrid","abstract":[{"lang":"eng","text":"We study concurrent graph games where n players cooperate against an opponent to reach a set of target states. Unlike traditional settings, we study distributed randomisation: team players do not share a source of randomness, and their private random sources are hidden from the opponent and from each other.\r\n\r\nWe show that memoryless strategies are sufficient for the threshold problem (deciding whether there is a strategy for the team that ensures winning with probability that exceeds a threshold), a result that not only places the problem in the Existential Theory of the Reals (ER) but also enables the construction of value iteration algorithms. We additionally show that the threshold problem is NP-hard. For the almost-sure reachability problem, we prove NP-completeness.\r\n\r\nWe introduce Individually Randomised Alternating-time Temporal Logic (IRATL). This logic extends the standard ATL framework to reason about probability thresholds, with semantics explicitly designed for coalitions that lack a shared source of randomness. On the practical side, we implement and evaluate a solver for the threshold and almost-sure problem based on the algorithms that we develop."}],"type":"conference","ddc":["000"],"department":[{"_id":"ToHe"},{"_id":"GradSch"}],"citation":{"chicago":"Brice, Leonard J, Thomas A Henzinger, Alipasha Montaseri, Ali Shafiee, and K. S. Thejaswini. “Randomise Alone, Reach as a Team.” In <i>38th International Conference on Computer Aided Verification</i>, 16682:215–36. Springer Nature, 2026. <a href=\"https://doi.org/10.1007/978-3-032-32519-8_12\">https://doi.org/10.1007/978-3-032-32519-8_12</a>.","mla":"Brice, Leonard J., et al. “Randomise Alone, Reach as a Team.” <i>38th International Conference on Computer Aided Verification</i>, vol. 16682, Springer Nature, 2026, pp. 215–36, doi:<a href=\"https://doi.org/10.1007/978-3-032-32519-8_12\">10.1007/978-3-032-32519-8_12</a>.","short":"L.J. Brice, T.A. Henzinger, A. Montaseri, A. Shafiee, K.S. Thejaswini, in:, 38th International Conference on Computer Aided Verification, Springer Nature, 2026, pp. 215–236.","ama":"Brice LJ, Henzinger TA, Montaseri A, Shafiee A, Thejaswini KS. Randomise alone, reach as a team. In: <i>38th International Conference on Computer Aided Verification</i>. Vol 16682. Springer Nature; 2026:215-236. doi:<a href=\"https://doi.org/10.1007/978-3-032-32519-8_12\">10.1007/978-3-032-32519-8_12</a>","ieee":"L. J. Brice, T. A. Henzinger, A. Montaseri, A. Shafiee, and K. S. Thejaswini, “Randomise alone, reach as a team,” in <i>38th International Conference on Computer Aided Verification</i>, Lisbon, Portugal, 2026, vol. 16682, pp. 215–236.","apa":"Brice, L. J., Henzinger, T. A., Montaseri, A., Shafiee, A., &#38; Thejaswini, K. S. (2026). Randomise alone, reach as a team. In <i>38th International Conference on Computer Aided Verification</i> (Vol. 16682, pp. 215–236). Lisbon, Portugal: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-032-32519-8_12\">https://doi.org/10.1007/978-3-032-32519-8_12</a>","ista":"Brice LJ, Henzinger TA, Montaseri A, Shafiee A, Thejaswini KS. 2026. Randomise alone, reach as a team. 38th International Conference on Computer Aided Verification. CAV: Computer Aided Verification vol. 16682, 215–236."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Springer Nature","author":[{"first_name":"Leonard J","full_name":"Brice, Leonard J","last_name":"Brice","id":"ce3b3409-db6c-11f0-aa64-ad678f7fd937"},{"orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"first_name":"Alipasha","full_name":"Montaseri, Alipasha","id":"709a7f96-8896-11f0-9809-d75612fc0f2e","last_name":"Montaseri"},{"id":"2783031a-7378-11f0-b2d0-f17f1db2ebad","last_name":"Shafiee","full_name":"Shafiee, Ali","first_name":"Ali"},{"full_name":"Thejaswini, K. S.","first_name":"K. S.","last_name":"Thejaswini"}],"doi":"10.1007/978-3-032-32519-8_12","OA_place":"publisher","oa_version":"Published Version","researchdata_availability":"yes","status":"public","external_id":{"arxiv":["2603.07094"]},"date_published":"2026-07-24T00:00:00Z","title":"Randomise alone, reach as a team"},{"external_id":{"arxiv":["2605.13185"]},"date_published":"2026-07-24T00:00:00Z","title":"Decoupled planning for multiple omega-regular objectives","researchdata_availability":"no","status":"public","doi":"10.1007/978-3-032-32519-8_13","oa_version":"Published Version","OA_place":"publisher","citation":{"apa":"Avni, G., Henzinger, T. A., Mallik, K., Sadhukhan, S., &#38; Thejaswini, K. S. (2026). Decoupled planning for multiple omega-regular objectives. In <i>38th International Conference on Computer Aided Verification</i> (Vol. 16682, pp. 237–257). Lisbon, Portugal: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-032-32519-8_13\">https://doi.org/10.1007/978-3-032-32519-8_13</a>","ista":"Avni G, Henzinger TA, Mallik K, Sadhukhan S, Thejaswini KS. 2026. Decoupled planning for multiple omega-regular objectives. 38th International Conference on Computer Aided Verification. CAV: Computer Aided Verification, LNCS, vol. 16682, 237–257.","ieee":"G. Avni, T. A. Henzinger, K. Mallik, S. Sadhukhan, and K. S. Thejaswini, “Decoupled planning for multiple omega-regular objectives,” in <i>38th International Conference on Computer Aided Verification</i>, Lisbon, Portugal, 2026, vol. 16682, pp. 237–257.","ama":"Avni G, Henzinger TA, Mallik K, Sadhukhan S, Thejaswini KS. Decoupled planning for multiple omega-regular objectives. In: <i>38th International Conference on Computer Aided Verification</i>. Vol 16682. Springer Nature; 2026:237-257. doi:<a href=\"https://doi.org/10.1007/978-3-032-32519-8_13\">10.1007/978-3-032-32519-8_13</a>","mla":"Avni, Guy, et al. “Decoupled Planning for Multiple Omega-Regular Objectives.” <i>38th International Conference on Computer Aided Verification</i>, vol. 16682, Springer Nature, 2026, pp. 237–57, doi:<a href=\"https://doi.org/10.1007/978-3-032-32519-8_13\">10.1007/978-3-032-32519-8_13</a>.","short":"G. Avni, T.A. Henzinger, K. Mallik, S. Sadhukhan, K.S. Thejaswini, in:, 38th International Conference on Computer Aided Verification, Springer Nature, 2026, pp. 237–257.","chicago":"Avni, Guy, Thomas A Henzinger, Kaushik Mallik, Suman Sadhukhan, and K. S. Thejaswini. “Decoupled Planning for Multiple Omega-Regular Objectives.” In <i>38th International Conference on Computer Aided Verification</i>, 16682:237–57. Springer Nature, 2026. <a href=\"https://doi.org/10.1007/978-3-032-32519-8_13\">https://doi.org/10.1007/978-3-032-32519-8_13</a>."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Springer Nature","author":[{"id":"463C8BC2-F248-11E8-B48F-1D18A9856A87","last_name":"Avni","orcid":"0000-0001-5588-8287","full_name":"Avni, Guy","first_name":"Guy"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0001-9864-7475","id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","last_name":"Mallik","first_name":"Kaushik","full_name":"Mallik, Kaushik"},{"last_name":"Sadhukhan","full_name":"Sadhukhan, Suman","first_name":"Suman"},{"last_name":"Thejaswini","full_name":"Thejaswini, K. S.","first_name":"K. S."}],"type":"conference","abstract":[{"lang":"eng","text":"We study the problem of generating paths on a graph that satisfy a collection of w-regular objectives. We propose a decoupled framework in which each objective is assigned to an independent agent that selects a local policy, while a scheduler—oblivious to the graph and objective—dynamically composes these policies into a single path. We ask when such a composition satisfies all objectives, assuming their conjunction is realizable. The framework enables modular policy design but raises fundamental compositional challenges. We show that even extremely fair deterministic schedulers do not ensure correctness, and that stochastic schedulers, while necessary, are insufficient without coordination. For safety objectives, we demonstrate that fully decentralized implementations are impossible, and we introduce a protocol for synchronizing on maximal safe actions. For non-safety objectives, we introduce conventions—simple, a priori restrictions agreed upon before the graph or objectives are revealed—that guarantee satisfaction of all objectives when followed by all agents. We characterize minimally restrictive conventions for major subclasses of w-regular objectives. In particular, Büchi objectives admit universal composition of finite-memory policies without scheduler communication; co-Büchi objectives require only knowledge of whether the agent was scheduled; and parity objectives additionally require knowledge of which agent was scheduled."}],"ddc":["000"],"department":[{"_id":"ToHe"}],"page":"237-257","OA_type":"hybrid","arxiv":1,"quality_controlled":"1","month":"07","publication":"38th International Conference on Computer Aided Verification","date_updated":"2026-08-18T08:41:44Z","volume":16682,"oa":1,"file_date_updated":"2026-08-18T08:40:07Z","supplementarymaterial":"no","publication_status":"published","has_accepted_license":"1","acknowledgement":"This work is funded by the following grants: European Research Council under Grant No.: ERC-2020-AdG 101020093, ISF grant no. 1679/21, grant RYC2024-049116, MICIU/AEI/10.13039/501100011033, the ESF+, and Volkswagen Foundation within its Momentum framework under project no. 9C283.","intvolume":"     16682","_id":"22719","language":[{"iso":"eng"}],"day":"24","tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"file":[{"date_created":"2026-08-18T08:40:07Z","file_size":531980,"relation":"main_file","checksum":"f17ba3f82854fdb4eb69fd922965661a","content_type":"application/pdf","access_level":"open_access","file_name":"2026_LNCS_Avni.pdf","file_id":"22730","creator":"dernst","success":1,"date_updated":"2026-08-18T08:40:07Z"}],"date_created":"2026-08-16T22:01:44Z","year":"2026","conference":{"start_date":"2026-07-26","name":"CAV: Computer Aided Verification","location":"Lisbon, Portugal","end_date":"2026-07-29"},"project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software"}],"alternative_title":["LNCS"],"article_processing_charge":"Yes (in subscription journal)","ec_funded":1,"das_tickbox":"0","scopus_import":"1","publication_identifier":{"issn":["0302-9743"],"isbn":["9783032325181"],"eissn":["1611-3349"]}},{"date_created":"2025-12-29T12:07:12Z","year":"2025","language":[{"iso":"eng"}],"_id":"20866","intvolume":"        62","day":"09","related_material":{"record":[{"relation":"earlier_version","status":"public","id":"14405"}]},"corr_author":"1","tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"file":[{"creator":"dernst","file_id":"20944","success":1,"date_updated":"2026-01-05T12:26:43Z","file_name":"2025_ActaInformatica_Bartocci.pdf","access_level":"open_access","content_type":"application/pdf","checksum":"06ed45a1218ad8464818803ae2968aaf","file_size":7117003,"date_created":"2026-01-05T12:26:43Z","relation":"main_file"}],"ec_funded":1,"scopus_import":"1","issue":"4","publication_identifier":{"issn":["0001-5903"],"eissn":["1432-0525"]},"project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020"},{"name":"Interface Theory for Security and Privacy","grant_number":"F8502","_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e"}],"article_processing_charge":"Yes (via OA deal)","abstract":[{"lang":"eng","text":"In this work, we present hypernode automata as a specification formalism for hyperproperties of systems whose executions may be misaligned among themselves, such as concurrent systems. These automata consist of nodes labeled with hypernode logic formulas and transitions marked with synchronizing actions. Hypernode logic formulas establish relations between sequences of variable values among different system executions. This logic enables both synchronous and asynchronous analysis of traces. In its asynchronous view on execution traces, hypernode formulas establish relations on the order of value changes for each variable without correlating their timing. In both views, the analysis of different execution traces is synchronized through the transitions of hypernode automata. By combining logic’s declarative nature with automata’s procedural power, hypernode automata seamlessly integrate asynchronicity requirements at the node level with synchronicity between node transitions. We show that the model-checking problem for hypernode automata is decidable for specifications where each node specifies either a synchronous or an asynchronous requirement for the system’s executions, but not both."}],"type":"journal_article","department":[{"_id":"ToHe"}],"ddc":["000"],"OA_type":"hybrid","article_type":"original","external_id":{"arxiv":["2305.02836"]},"article_number":"43","date_published":"2025-12-09T00:00:00Z","title":"Hypernode automata","status":"public","doi":"10.1007/s00236-025-00509-8","oa_version":"Published Version","OA_place":"publisher","publisher":"Springer Nature","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"apa":"Bartocci, E., Chalupa, M., Henzinger, T. A., Nickovic, D., &#38; Oliveira da Costa, A. (2025). Hypernode automata. <i>Acta Informatica</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s00236-025-00509-8\">https://doi.org/10.1007/s00236-025-00509-8</a>","ista":"Bartocci E, Chalupa M, Henzinger TA, Nickovic D, Oliveira da Costa A. 2025. Hypernode automata. Acta Informatica. 62(4), 43.","ieee":"E. Bartocci, M. Chalupa, T. A. Henzinger, D. Nickovic, and A. Oliveira da Costa, “Hypernode automata,” <i>Acta Informatica</i>, vol. 62, no. 4. Springer Nature, 2025.","ama":"Bartocci E, Chalupa M, Henzinger TA, Nickovic D, Oliveira da Costa A. Hypernode automata. <i>Acta Informatica</i>. 2025;62(4). doi:<a href=\"https://doi.org/10.1007/s00236-025-00509-8\">10.1007/s00236-025-00509-8</a>","short":"E. Bartocci, M. Chalupa, T.A. Henzinger, D. Nickovic, A. Oliveira da Costa, Acta Informatica 62 (2025).","mla":"Bartocci, Ezio, et al. “Hypernode Automata.” <i>Acta Informatica</i>, vol. 62, no. 4, 43, Springer Nature, 2025, doi:<a href=\"https://doi.org/10.1007/s00236-025-00509-8\">10.1007/s00236-025-00509-8</a>.","chicago":"Bartocci, Ezio, Marek Chalupa, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira da Costa. “Hypernode Automata.” <i>Acta Informatica</i>. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/s00236-025-00509-8\">https://doi.org/10.1007/s00236-025-00509-8</a>."},"author":[{"last_name":"Bartocci","full_name":"Bartocci, Ezio","first_name":"Ezio"},{"first_name":"Marek","full_name":"Chalupa, Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","last_name":"Chalupa"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Dejan","full_name":"Nickovic, Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","last_name":"Nickovic"},{"id":"f347ec37-6676-11ee-b395-a888cb7b4fb4","last_name":"Oliveira da Costa","orcid":"0000-0002-8741-5799","full_name":"Oliveira da Costa, Ana","first_name":"Ana"}],"oa":1,"file_date_updated":"2026-01-05T12:26:43Z","publication_status":"published","acknowledgement":"This work was supported in part by the Austrian Science Fund (FWF) SFB project SpyCoDe 10.55776/F85, by the FWF projects ZK-35 and W1255-N23, and by the ERC Advanced Grant VAMOS 101020093. Open access funding provided by Institute of Science and Technology (IST Austria).","has_accepted_license":"1","arxiv":1,"quality_controlled":"1","month":"12","publication":"Acta Informatica","date_updated":"2026-01-05T12:27:41Z","volume":62},{"project":[{"call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"},{"_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e","grant_number":"F8502","name":"Interface Theory for Security and Privacy"}],"article_processing_charge":"Yes (via OA deal)","ec_funded":1,"publication_identifier":{"isbn":["9798400715259"]},"scopus_import":"1","related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"21401"}]},"corr_author":"1","file":[{"date_created":"2026-01-21T07:34:58Z","file_size":1241912,"relation":"main_file","content_type":"application/pdf","checksum":"615ffddab6c7285158c2953acec6fa6f","access_level":"open_access","file_name":"2025_CCS_HenzingerT.pdf","success":1,"creator":"dernst","file_id":"21024","date_updated":"2026-01-21T07:34:58Z"}],"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"language":[{"iso":"eng"}],"_id":"21020","day":"22","date_created":"2026-01-20T10:17:10Z","year":"2025","conference":{"start_date":"2025-10-13","name":"CCS: Conference on Computer and Communications Security","end_date":"2025-10-17","location":"Taipei, Taiwan"},"publication":"Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security","arxiv":1,"month":"11","quality_controlled":"1","date_updated":"2026-03-13T13:37:19Z","publication_status":"published","oa":1,"file_date_updated":"2026-01-21T07:34:58Z","has_accepted_license":"1","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","external_id":{"arxiv":["2505.09276"]},"date_published":"2025-11-22T00:00:00Z","title":"Privacy-preserving runtime verification","citation":{"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>.","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.","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>.","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.","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>","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.","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>"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Association for Computing Machinery","author":[{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Mahyar","full_name":"Karimi, Mahyar","orcid":"0009-0005-0820-1696","last_name":"Karimi","id":"6e5417ba-5355-11ee-ae5a-94c2e510b26b"},{"full_name":"Thejaswini, K. S.","first_name":"K. S.","last_name":"Thejaswini","id":"3807fb92-fdc1-11ee-bb4a-b4d8a431c753"}],"doi":"10.1145/3719027.3765137","OA_place":"publisher","oa_version":"Published Version","abstract":[{"lang":"eng","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."}],"type":"conference","ddc":["000"],"department":[{"_id":"ToHe"},{"_id":"GradSch"}],"OA_type":"hybrid","page":"2774-2787"},{"oa":1,"file_date_updated":"2026-02-11T09:33:20Z","publication_status":"published","has_accepted_license":"1","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.","arxiv":1,"quality_controlled":"1","month":"12","publication":"45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science","date_updated":"2026-02-11T09:35:04Z","volume":360,"type":"conference","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."}],"ddc":["000"],"department":[{"_id":"ToHe"}],"page":"20:1-20:18","OA_type":"gold","external_id":{"arxiv":["2510.12298"]},"date_published":"2025-12-09T00:00:00Z","title":"Flavors of quantifiers in hyperlogics","status":"public","doi":"10.4230/LIPICS.FSTTCS.2025.20","OA_place":"publisher","oa_version":"Published Version","citation":{"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>","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>","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>."},"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"first_name":"Marek","full_name":"Chalupa, Marek","last_name":"Chalupa","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463"},{"orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"id":"8b282559-50b0-11ef-861e-d6ace0d92e9b","last_name":"Oliveira da Costa","full_name":"Oliveira da Costa, Ana A","first_name":"Ana A"}],"ec_funded":1,"scopus_import":"1","project":[{"name":"Interface Theory for Security and Privacy","_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e","grant_number":"F8502"},{"call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"alternative_title":["LIPIcs"],"article_processing_charge":"No","year":"2025","date_created":"2026-01-29T15:39:15Z","conference":{"end_date":"2025-12-19","location":"Pilani, India","name":"FSTTCS: Conference on Foundations of Software Technology and Theoretical Computer Science","start_date":"2025-12-17"},"language":[{"iso":"eng"}],"_id":"21089","intvolume":"       360","day":"09","corr_author":"1","file":[{"file_name":"2025_LIPIcS_Chalupa.pdf","date_updated":"2026-02-11T09:33:20Z","creator":"dernst","file_id":"21213","success":1,"relation":"main_file","date_created":"2026-02-11T09:33:20Z","file_size":933970,"access_level":"open_access","checksum":"8188ee5c7b14193d48eeb655e9bbdc47","content_type":"application/pdf"}],"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"}},{"oa":1,"publication_status":"published","acknowledgement":"This work is supported by the European Research Council under Grant No.: ERC-2020-AdG 101020093.","quality_controlled":"1","month":"09","arxiv":1,"publication":"25th International Conference on Runtime Verification","date_updated":"2026-02-16T11:57:00Z","volume":16087,"department":[{"_id":"ToHe"}],"abstract":[{"lang":"eng","text":"Fairness in AI is traditionally studied as a static property evaluated once, over a fixed dataset. However, real-world AI systems operate sequentially, with outcomes and environments evolving over time. This paper proposes a framework for analysing fairness as a runtime property. Using a minimal yet expressive model based on sequences of coin tosses with possibly evolving biases, we study the problems of monitoring and enforcing fairness expressed in either toss outcomes or coin biases. Since there is no one-size-fits-all solution for either problem, we provide a summary of monitoring and enforcement strategies, parametrised by environment dynamics, prediction horizon, and confidence thresholds. For both problems, we present general results under simple or minimal assumptions. We survey existing solutions for the monitoring problem for Markovian and additive dynamics, and existing solutions for the enforcement problem in static settings with known dynamics."}],"type":"conference","page":"1-21","OA_type":"green","date_published":"2025-09-13T00:00:00Z","title":"Algorithmic fairness: A runtime perspective","external_id":{"arxiv":["2507.20711"]},"status":"public","OA_place":"repository","oa_version":"Preprint","doi":"10.1007/978-3-032-05435-7_1","author":[{"orcid":"0000-0002-0783-904X","id":"708cad98-e86a-11ef-8098-bdae2d7c6af1","last_name":"Cano Cordoba","first_name":"Filip","full_name":"Cano Cordoba, Filip"},{"orcid":"0000-0002-2985-7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"full_name":"Kueffner, Konstantin","first_name":"Konstantin","orcid":"0000-0001-8974-2542","last_name":"Kueffner","id":"8121a2d0-dc85-11ea-9058-af578f3b4515"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"apa":"Cano Cordoba, F., Henzinger, T. A., &#38; Kueffner, K. (2025). Algorithmic fairness: A runtime perspective. In <i>25th International Conference on Runtime Verification</i> (Vol. 16087, pp. 1–21). Graz, Austria: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-032-05435-7_1\">https://doi.org/10.1007/978-3-032-05435-7_1</a>","ista":"Cano Cordoba F, Henzinger TA, Kueffner K. 2025. Algorithmic fairness: A runtime perspective. 25th International Conference on Runtime Verification. RV: Runtime Verification, LNCS, vol. 16087, 1–21.","ieee":"F. Cano Cordoba, T. A. Henzinger, and K. Kueffner, “Algorithmic fairness: A runtime perspective,” in <i>25th International Conference on Runtime Verification</i>, Graz, Austria, 2025, vol. 16087, pp. 1–21.","ama":"Cano Cordoba F, Henzinger TA, Kueffner K. Algorithmic fairness: A runtime perspective. In: <i>25th International Conference on Runtime Verification</i>. Vol 16087. Springer Nature; 2025:1-21. doi:<a href=\"https://doi.org/10.1007/978-3-032-05435-7_1\">10.1007/978-3-032-05435-7_1</a>","short":"F. Cano Cordoba, T.A. Henzinger, K. Kueffner, in:, 25th International Conference on Runtime Verification, Springer Nature, 2025, pp. 1–21.","mla":"Cano Cordoba, Filip, et al. “Algorithmic Fairness: A Runtime Perspective.” <i>25th International Conference on Runtime Verification</i>, vol. 16087, Springer Nature, 2025, pp. 1–21, doi:<a href=\"https://doi.org/10.1007/978-3-032-05435-7_1\">10.1007/978-3-032-05435-7_1</a>.","chicago":"Cano Cordoba, Filip, Thomas A Henzinger, and Konstantin Kueffner. “Algorithmic Fairness: A Runtime Perspective.” In <i>25th International Conference on Runtime Verification</i>, 16087:1–21. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-032-05435-7_1\">https://doi.org/10.1007/978-3-032-05435-7_1</a>."},"publisher":"Springer Nature","ec_funded":1,"publication_identifier":{"eisbn":["9783032054357"],"eissn":["1611-3349"],"issn":["0302-9743"]},"project":[{"call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"alternative_title":["LNCS"],"article_processing_charge":"No","year":"2025","date_created":"2026-01-29T16:01:41Z","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2507.20711","open_access":"1"}],"conference":{"start_date":"2025-09-15","name":"RV: Runtime Verification","location":"Graz, Austria","end_date":"2025-09-19"},"day":"13","_id":"21090","language":[{"iso":"eng"}],"intvolume":"     16087","corr_author":"1"},{"publication_identifier":{"eisbn":["9783032054357"],"eissn":["1611-3349"],"issn":["0302-9743"]},"ec_funded":1,"article_processing_charge":"No","project":[{"call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093"}],"alternative_title":["LNCS"],"main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2507.11987"}],"conference":{"location":"Graz, Austria","end_date":"2025-09-19","name":"RV: Runtime Verification","start_date":"2025-09-15"},"date_created":"2026-01-29T16:03:01Z","year":"2025","intvolume":"     16087","_id":"21091","language":[{"iso":"eng"}],"day":"13","corr_author":"1","acknowledgement":"This work is supported by the European Research Council under Grant No.: ERC-2020-AdG 101020093.","oa":1,"publication_status":"published","date_updated":"2026-02-16T11:53:25Z","volume":16087,"arxiv":1,"quality_controlled":"1","month":"09","publication":"25th International Conference on Runtime Verification","OA_type":"green","page":"54-72","abstract":[{"lang":"eng","text":"Neural certificates have emerged as a powerful tool in cyber-physical systems control, providing witnesses of correctness. These certificates, such as barrier functions, often learned alongside control policies, once verified, serve as mathematical proofs of system safety. However, traditional formal verification of their defining conditions typically faces scalability challenges due to exhaustive state-space exploration. To address this challenge, we propose a lightweight runtime monitoring framework that integrates real-time verification and does not require access to the underlying control policy. Our monitor observes the system during deployment and performs on-the-fly verification of the certificate over a lookahead region to ensure safety within a finite prediction horizon. We instantiate this framework for ReLU-based control barrier functions and demonstrate its practical effectiveness in a case study. Our approach enables timely detection of safety violations and incorrect certificates with minimal overhead, providing an effective but lightweight alternative to the static verification of the certificates."}],"type":"conference","department":[{"_id":"ToHe"}],"doi":"10.1007/978-3-032-05435-7_4","OA_place":"repository","oa_version":"Preprint","citation":{"short":"T.A. Henzinger, K. Kueffner, E. Yu, in:, 25th International Conference on Runtime Verification, Springer Nature, 2025, pp. 54–72.","mla":"Henzinger, Thomas A., et al. “Formal Verification of Neural Certificates Done Dynamically.” <i>25th International Conference on Runtime Verification</i>, vol. 16087, Springer Nature, 2025, pp. 54–72, doi:<a href=\"https://doi.org/10.1007/978-3-032-05435-7_4\">10.1007/978-3-032-05435-7_4</a>.","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>.","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.","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>","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.","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>"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Springer Nature","author":[{"orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"first_name":"Konstantin","full_name":"Kueffner, Konstantin","orcid":"0000-0001-8974-2542","id":"8121a2d0-dc85-11ea-9058-af578f3b4515","last_name":"Kueffner"},{"first_name":"Zhengqi","full_name":"Yu, Zhengqi","orcid":"0000-0002-4993-773X","last_name":"Yu","id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342"}],"external_id":{"arxiv":["2507.11987"]},"date_published":"2025-09-13T00:00:00Z","title":"Formal verification of neural certificates done dynamically","status":"public"},{"alternative_title":["LNCS"],"project":[{"grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software"}],"article_processing_charge":"No","ec_funded":1,"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"eisbn":["9783032054357"]},"corr_author":"1","intvolume":"     16087","_id":"21092","language":[{"iso":"eng"}],"day":"13","date_created":"2026-01-29T16:03:43Z","year":"2025","conference":{"end_date":"2025-09-19","location":"Graz, Austria","start_date":"2025-09-15","name":"RV: Runtime Verification"},"main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2508.00021","open_access":"1"}],"publication":"25th International Conference on Runtime Verification","arxiv":1,"month":"09","quality_controlled":"1","volume":16087,"date_updated":"2026-02-16T11:56:38Z","publication_status":"published","oa":1,"acknowledgement":"This work is supported by the European Research Council under Grant No.: ERC-2020-AdG 101020093.","status":"public","external_id":{"arxiv":["2508.00021"]},"title":"Alignment monitoring","date_published":"2025-09-13T00:00:00Z","publisher":"Springer Nature","citation":{"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>","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.","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.","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>","short":"T.A. Henzinger, K. Kueffner, V. Singh, I. Sun, in:, 25th International Conference on Runtime Verification, Springer Nature, 2025, pp. 140–159.","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>.","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>."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"first_name":"Konstantin","full_name":"Kueffner, Konstantin","id":"8121a2d0-dc85-11ea-9058-af578f3b4515","last_name":"Kueffner","orcid":"0000-0001-8974-2542"},{"full_name":"Singh, Vasu","first_name":"Vasu","id":"4DAE2708-F248-11E8-B48F-1D18A9856A87","last_name":"Singh"},{"full_name":"Sun, I","first_name":"I","last_name":"Sun"}],"doi":"10.1007/978-3-032-05435-7_9","OA_place":"repository","oa_version":"Preprint","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."}],"type":"conference","department":[{"_id":"ToHe"}],"page":"140-159","OA_type":"green"},{"external_id":{"arxiv":["2508.02301"]},"date_published":"2025-09-13T00:00:00Z","title":"Monitoring hypernode logic over infinite domains","status":"public","doi":"10.1007/978-3-032-05435-7_23","oa_version":"Preprint","OA_place":"repository","citation":{"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>.","short":"M. Chalupa, T.A. Henzinger, A.A. Oliveira da Costa, in:, 25th International Conference on Runtime Verification, Springer Nature, 2025, pp. 417–437.","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>.","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>","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.","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.","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>"},"publisher":"Springer Nature","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"first_name":"Marek","full_name":"Chalupa, Marek","last_name":"Chalupa","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463"},{"orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"full_name":"Oliveira da Costa, Ana A","first_name":"Ana A","last_name":"Oliveira da Costa","id":"8b282559-50b0-11ef-861e-d6ace0d92e9b"}],"type":"conference","abstract":[{"lang":"eng","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."}],"department":[{"_id":"ToHe"}],"page":"417-437","OA_type":"green","arxiv":1,"month":"09","quality_controlled":"1","publication":"25th International Conference on Runtime Verification","date_updated":"2026-02-16T11:59:20Z","volume":16087,"oa":1,"publication_status":"published","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093 and in part by the FWF-2022-SFB F8502 (SPyCoDe).","language":[{"iso":"eng"}],"_id":"21093","intvolume":"     16087","day":"13","corr_author":"1","year":"2025","date_created":"2026-01-29T16:04:31Z","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2508.02301","open_access":"1"}],"conference":{"start_date":"2025-09-15","name":"RV: Runtime Verification","location":"Graz, Austria","end_date":"2025-09-19"},"project":[{"call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093"},{"grant_number":"F8502","_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e","name":"Interface Theory for Security and Privacy"}],"alternative_title":["LNCS"],"article_processing_charge":"No","ec_funded":1,"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"eisbn":["9783032054357"]}},{"publication":"45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science","arxiv":1,"quality_controlled":"1","month":"12","volume":360,"date_updated":"2026-02-19T09:39:15Z","publication_status":"published","oa":1,"file_date_updated":"2026-02-18T09:13:25Z","has_accepted_license":"1","acknowledgement":"This work is a part of project VAMOS that has received funding from the European\r\nResearch Council (ERC), grant agreement No 101020093.\r\n","status":"public","external_id":{"arxiv":["2508.15356"]},"date_published":"2025-12-09T00:00:00Z","title":"ε-stationary Nash equilibria in multi-player stochastic graph games","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"apa":"Asadi, A., Brice, L., Chatterjee, K., &#38; Thejaswini, K. S. (2025). ε-stationary Nash equilibria in multi-player stochastic graph games. In <i>45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i> (Vol. 360, p. 9:1-9:17). Pilani, India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/lipics.fsttcs.2025.9\">https://doi.org/10.4230/lipics.fsttcs.2025.9</a>","ista":"Asadi A, Brice L, Chatterjee K, Thejaswini KS. 2025. ε-stationary Nash equilibria in multi-player stochastic graph games. 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, 9:1-9:17.","ieee":"A. Asadi, L. Brice, K. Chatterjee, and K. S. Thejaswini, “ε-stationary Nash equilibria in multi-player stochastic graph games,” in <i>45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>, Pilani, India, 2025, vol. 360, p. 9:1-9:17.","ama":"Asadi A, Brice L, Chatterjee K, Thejaswini KS. ε-stationary Nash equilibria in multi-player stochastic graph games. 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:9:1-9:17. doi:<a href=\"https://doi.org/10.4230/lipics.fsttcs.2025.9\">10.4230/lipics.fsttcs.2025.9</a>","mla":"Asadi, Ali, et al. “ε-Stationary Nash Equilibria in Multi-Player Stochastic Graph Games.” <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. 9:1-9:17, doi:<a href=\"https://doi.org/10.4230/lipics.fsttcs.2025.9\">10.4230/lipics.fsttcs.2025.9</a>.","short":"A. Asadi, L. Brice, K. Chatterjee, K.S. Thejaswini, in:, 45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025, p. 9:1-9:17.","chicago":"Asadi, Ali, Leonard Brice, Krishnendu Chatterjee, and K. S. Thejaswini. “ε-Stationary Nash Equilibria in Multi-Player Stochastic Graph Games.” In <i>45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>, 360:9:1-9:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. <a href=\"https://doi.org/10.4230/lipics.fsttcs.2025.9\">https://doi.org/10.4230/lipics.fsttcs.2025.9</a>."},"author":[{"first_name":"Ali","full_name":"Asadi, Ali","last_name":"Asadi","id":"02d96aae-000e-11ec-b801-cadd0a5eefbb"},{"first_name":"Leonard","full_name":"Brice, Leonard","last_name":"Brice"},{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"full_name":"Thejaswini, K. S.","first_name":"K. S.","last_name":"Thejaswini","id":"3807fb92-fdc1-11ee-bb4a-b4d8a431c753"}],"doi":"10.4230/lipics.fsttcs.2025.9","oa_version":"Published Version","OA_place":"publisher","type":"conference","abstract":[{"lang":"eng","text":"A strategy profile in a multi-player game is a Nash equilibrium if no player can unilaterally deviate to achieve a strictly better payoff. A profile is an ε-Nash equilibrium if no player can gain more than ε by unilaterally deviating from their strategy. In this work, we use ε-Nash equilibria to approximate the computation of Nash equilibria. Specifically, we focus on turn-based, multiplayer stochastic games played on graphs, where players are restricted to stationary strategies - strategies that use randomness but not memory.\r\nThe problem of deciding the constrained existence of stationary Nash equilibria - where each player’s payoff must lie within a given interval - is known to be ∃ℝ-complete in such a setting (Hansen and Sølvsten, 2020). We extend this line of work to stationary ε-Nash equilibria and present an algorithm that solves the following promise problem: given a game with a Nash equilibrium satisfying the constraints, compute an ε-Nash equilibrium that ε-satisfies those same constraints - satisfies the constraints up to an ε additive error. Our algorithm runs in FNP^NP time.\r\nTo achieve this, we first show that if a constrained Nash equilibrium exists, then one exists where the non-zero probabilities are at least an inverse of a double-exponential in the input. We further prove that such a strategy can be encoded using floating-point representations, as in the work of Frederiksen and Miltersen (2013), which finally gives us our FNP^NP algorithm. \r\nWe further show that the decision version of the promise problem is NP-hard. Finally, we show a partial tightness result by proving a lower bound for such techniques: if a constrained Nash equilibrium exists, then there must be one where the probabilities in the strategies are double-exponentially small."}],"department":[{"_id":"KrCh"},{"_id":"GradSch"}],"ddc":["000"],"page":"9:1-9:17","OA_type":"gold","alternative_title":["LIPIcs"],"project":[{"name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"article_processing_charge":"Yes","ec_funded":1,"publication_identifier":{"isbn":["9783959774062"]},"corr_author":"1","tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"file":[{"date_created":"2026-02-18T09:13:25Z","file_size":1054007,"relation":"main_file","checksum":"a66343e3ccc4a9cc5bc699c03d5764ff","content_type":"application/pdf","access_level":"open_access","file_name":"2025_FSTTCS_Asadi.pdf","file_id":"21316","creator":"dernst","success":1,"date_updated":"2026-02-18T09:13:25Z"}],"_id":"21281","intvolume":"       360","language":[{"iso":"eng"}],"day":"09","date_created":"2026-02-17T08:27:14Z","year":"2025","conference":{"name":"FSTTCS: Conference on Foundations of Software Technology and Theoretical Computer Science","start_date":"2025-12-17","location":"Pilani, India","end_date":"2025-12-19"}},{"ec_funded":1,"publication_identifier":{"issn":["0925-9856"],"eissn":["1572-8102"]},"scopus_import":"1","project":[{"grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020"},{"name":"Interface Theory for Security and Privacy","grant_number":"F8502","_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e"}],"article_processing_charge":"Yes (via OA deal)","date_created":"2024-06-02T22:00:57Z","year":"2025","isi":1,"related_material":{"record":[{"relation":"shorter_version","status":"public","id":"11355"}]},"corr_author":"1","file":[{"file_name":"2025_FormalMethodsSysDesign_Bartocci.pdf","creator":"dernst","success":1,"file_id":"20879","date_updated":"2025-12-30T06:50:12Z","file_size":3860690,"date_created":"2025-12-30T06:50:12Z","relation":"main_file","access_level":"open_access","checksum":"244a71a916103b8ea08e9d0bab32bcd9","content_type":"application/pdf"}],"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"intvolume":"        66","_id":"17094","language":[{"iso":"eng"}],"day":"01","publication_status":"published","oa":1,"file_date_updated":"2025-12-30T06:50:12Z","PlanS_conform":"1","has_accepted_license":"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].","publication":"Formal Methods in System Design","arxiv":1,"month":"05","quality_controlled":"1","volume":66,"date_updated":"2025-12-30T06:50:51Z","type":"journal_article","abstract":[{"lang":"eng","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."}],"ddc":["000"],"department":[{"_id":"ToHe"}],"OA_type":"hybrid","page":"3-48","article_type":"original","status":"public","external_id":{"isi":["001230084200001"],"arxiv":["2002.06465"]},"date_published":"2025-05-01T00:00:00Z","title":"Information-flow interfaces","citation":{"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.","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>.","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>","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.","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>","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."},"publisher":"Springer Nature","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"last_name":"Bartocci","first_name":"Ezio","full_name":"Bartocci, Ezio"},{"full_name":"Ferrere, Thomas","first_name":"Thomas","orcid":"0000-0001-5199-3143","last_name":"Ferrere","id":"40960E6E-F248-11E8-B48F-1D18A9856A87"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000-0002-2985-7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A"},{"last_name":"Nickovic","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","full_name":"Nickovic, Dejan","first_name":"Dejan"},{"first_name":"Ana","full_name":"Oliveira da Costa, Ana","orcid":"0000-0002-8741-5799","last_name":"Oliveira da Costa","id":"f347ec37-6676-11ee-b395-a888cb7b4fb4"}],"doi":"10.1007/s10703-024-00447-0","OA_place":"publisher","oa_version":"Published Version"},{"oa":1,"publication_status":"published","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.","arxiv":1,"month":"04","quality_controlled":"1","publication":"Proceedings of the 39th AAAI Conference on Artificial Intelligence","date_updated":"2026-02-16T12:24:30Z","volume":39,"type":"conference","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."}],"department":[{"_id":"ToHe"}],"page":"15659-15668","OA_type":"green","external_id":{"arxiv":["2412.11994"]},"date_published":"2025-04-11T00:00:00Z","title":"Fairness shields: Safeguarding against biased decision makers","status":"public","doi":"10.1609/aaai.v39i15.33719","OA_place":"repository","oa_version":"Preprint","citation":{"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.","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>.","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>","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.","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>","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."},"publisher":"Association for the Advancement of Artificial Intelligence","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"orcid":"0000-0002-0783-904X","id":"708cad98-e86a-11ef-8098-bdae2d7c6af1","last_name":"Cano Cordoba","full_name":"Cano Cordoba, Filip","first_name":"Filip"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A"},{"full_name":"Könighofer, Bettina","first_name":"Bettina","last_name":"Könighofer"},{"id":"8121a2d0-dc85-11ea-9058-af578f3b4515","last_name":"Kueffner","orcid":"0000-0001-8974-2542","first_name":"Konstantin","full_name":"Kueffner, Konstantin"},{"id":"0834ff3c-6d72-11ec-94e0-b5b0a4fb8598","last_name":"Mallik","orcid":"0000-0001-9864-7475","full_name":"Mallik, Kaushik","first_name":"Kaushik"}],"ec_funded":1,"scopus_import":"1","issue":"15","publication_identifier":{"eissn":["2374-3468"],"issn":["2159-5399"]},"project":[{"name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"article_processing_charge":"No","year":"2025","date_created":"2025-05-11T22:02:39Z","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2412.11994","open_access":"1"}],"conference":{"end_date":"2025-03-04","location":"Philadelphia, PA, United States","name":"AAAI: Conference on Artificial Intelligence","start_date":"2025-02-25"},"_id":"19665","language":[{"iso":"eng"}],"intvolume":"        39","day":"11","corr_author":"1"},{"page":"26409-26417","OA_type":"green","type":"conference","abstract":[{"lang":"eng","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."}],"department":[{"_id":"ToHe"}],"doi":"10.1609/aaai.v39i25.34840","OA_place":"repository","oa_version":"Preprint","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"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.","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>","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.","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>","mla":"Yu, Emily, et al. “Neural Control and Certificate Repair via Runtime Monitoring.” <i>Proceedings of the 39th AAAI Conference on Artificial Intelligence</i>, vol. 39, no. 25, Association for the Advancement of Artificial Intelligence, 2025, pp. 26409–17, doi:<a href=\"https://doi.org/10.1609/aaai.v39i25.34840\">10.1609/aaai.v39i25.34840</a>.","short":"E. Yu, D. Zikelic, T.A. Henzinger, in:, Proceedings of the 39th AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2025, pp. 26409–26417.","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>."},"publisher":"Association for the Advancement of Artificial Intelligence","author":[{"id":"20aa2ae8-f2f1-11ed-bbfa-8205053f1342","last_name":"Yu","full_name":"Yu, Zhengqi","first_name":"Zhengqi"},{"orcid":"0000-0002-4681-1699","last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","full_name":"Zikelic, Dorde","first_name":"Dorde"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","orcid":"0000-0002-2985-7724","first_name":"Thomas A","full_name":"Henzinger, Thomas A"}],"external_id":{"arxiv":["2412.12996"]},"title":"Neural control and certificate repair via runtime monitoring","date_published":"2025-04-11T00:00:00Z","status":"public","acknowledgement":"This work was supported in part by the ERC project ERC2020-AdG 101020093","oa":1,"publication_status":"published","date_updated":"2025-05-12T09:49:25Z","volume":39,"arxiv":1,"quality_controlled":"1","month":"04","publication":"Proceedings of the 39th AAAI Conference on Artificial Intelligence","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2412.12996","open_access":"1"}],"conference":{"end_date":"2025-03-04","location":"Philadelphia, PA, United States","start_date":"2025-02-25","name":"AAAI: Conference on Artificial Intelligence"},"year":"2025","date_created":"2025-05-11T22:02:40Z","_id":"19668","language":[{"iso":"eng"}],"intvolume":"        39","day":"11","corr_author":"1","scopus_import":"1","issue":"25","publication_identifier":{"eissn":["2374-3468"],"issn":["2159-5399"]},"ec_funded":1,"article_processing_charge":"No","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software"}]},{"title":"BUBAAK: Dynamic cooperative verification","date_published":"2025-05-01T00:00:00Z","status":"public","doi":"10.1007/978-3-031-90660-2_14","OA_place":"publisher","oa_version":"Published Version","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","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.","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>.","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>.","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.","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>","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.","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>"},"publisher":"Springer Nature","author":[{"id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","last_name":"Chalupa","full_name":"Chalupa, Marek","first_name":"Marek"},{"full_name":"Richter, Cedric","first_name":"Cedric","last_name":"Richter"}],"type":"conference","abstract":[{"lang":"eng","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."}],"ddc":["000"],"department":[{"_id":"ToHe"}],"OA_type":"hybrid","page":"212-216","quality_controlled":"1","month":"05","publication":"31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems","date_updated":"2025-06-02T07:21:41Z","volume":15698,"oa":1,"file_date_updated":"2025-06-02T07:10:35Z","publication_status":"published","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).","has_accepted_license":"1","intvolume":"     15698","_id":"19739","language":[{"iso":"eng"}],"day":"01","corr_author":"1","file":[{"access_level":"open_access","checksum":"3f604f25dbe37383acb7f8308aad3ca6","content_type":"application/pdf","relation":"main_file","date_created":"2025-06-02T07:10:35Z","file_size":259050,"date_updated":"2025-06-02T07:10:35Z","file_id":"19766","success":1,"creator":"dernst","file_name":"2025_TACAS_Chalupa.pdf"}],"tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"date_created":"2025-05-25T22:17:04Z","year":"2025","conference":{"location":"Hamilton, ON, Canada","end_date":"2025-05-08","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2025-05-03"},"project":[{"name":"Vigilant Algorithmic Monitoring of Software","call_identifier":"H2020","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"alternative_title":["LNCS"],"article_processing_charge":"No","ec_funded":1,"scopus_import":"1","publication_identifier":{"eissn":["1611-3349"],"isbn":["9783031906596"],"issn":["0302-9743"]}}]