[{"date_updated":"2026-02-12T13:39:07Z","day":"01","project":[{"grant_number":"F8502","name":"Interface Theory for Security and Privacy","_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e"},{"_id":"7bdd2f70-9f16-11ee-852c-b7950bc6d277","name":"SeCure, privAte, and interoperabLe layEr 2","grant_number":"ICT22-045"}],"publisher":"Springer Nature","author":[{"orcid":"0000-0001-7227-8309","id":"f09651b9-fec0-11ec-b5d8-934aff0e52a4","first_name":"Ray","last_name":"Neiheiser","full_name":"Neiheiser, Ray"},{"first_name":"Eleftherios","id":"f5983044-d7ef-11ea-ac6d-fd1430a26d30","orcid":"0000-0002-8827-3382","full_name":"Kokoris Kogias, Eleftherios","last_name":"Kokoris Kogias"}],"type":"conference","oa_version":"Preprint","conference":{"location":"Miyakojima, Japan","start_date":"2025-04-14","name":"FC: Financial Cryptography and Data Security","end_date":"2025-04-18"},"publication":"29th International Conference on Financial Cryptography and Data Security","corr_author":"1","abstract":[{"lang":"eng","text":"Many blockchains such as Ethereum execute all incoming transactions sequentially significantly limiting the potential throughput. A common approach to scale execution is parallel execution engines that fully utilize modern multi-core architectures. Parallel execution is then either done optimistically, by executing transactions in parallel and detecting conflicts on the fly, or guided, by requiring exhaustive client transaction hints and scheduling transactions accordingly.\r\n\r\nHowever, recent studies have shown that the performance of parallel execution engines depends on the nature of the underlying workload. In fact, in some cases, only a 60% speed-up compared to sequential execution could be obtained. This is the case, as transactions that access the same resources must be executed sequentially. For example, if 10% of the transactions in a block access the same resource, the execution cannot meaningfully scale beyond 10 cores. Therefore, a single popular application can bottleneck the execution and limit the potential throughput.\r\n\r\nIn this paper, we introduce Anthemius, a block construction algorithm that optimizes parallel transaction execution throughput. We evaluate Anthemius exhaustively under a range of workloads, and show that Anthemius enables the underlying parallel execution engine to process over twice as many transactions."}],"status":"public","OA_type":"green","language":[{"iso":"eng"}],"date_published":"2026-01-01T00:00:00Z","volume":15751,"page":"307-323","doi":"10.1007/978-3-032-07024-1_18","article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"21042","publication_identifier":{"eissn":["1611-3349"],"isbn":["9783032070234"],"issn":["0302-9743"]},"OA_place":"repository","citation":{"ama":"Neiheiser R, Kokoris Kogias E. Anthemius: Efficient and modular block assembly for concurrent execution. In: <i>29th International Conference on Financial Cryptography and Data Security</i>. Vol 15751. Springer Nature; 2026:307-323. doi:<a href=\"https://doi.org/10.1007/978-3-032-07024-1_18\">10.1007/978-3-032-07024-1_18</a>","apa":"Neiheiser, R., &#38; Kokoris Kogias, E. (2026). Anthemius: Efficient and modular block assembly for concurrent execution. In <i>29th International Conference on Financial Cryptography and Data Security</i> (Vol. 15751, pp. 307–323). Miyakojima, Japan: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-032-07024-1_18\">https://doi.org/10.1007/978-3-032-07024-1_18</a>","short":"R. Neiheiser, E. Kokoris Kogias, in:, 29th International Conference on Financial Cryptography and Data Security, Springer Nature, 2026, pp. 307–323.","ista":"Neiheiser R, Kokoris Kogias E. 2026. Anthemius: Efficient and modular block assembly for concurrent execution. 29th International Conference on Financial Cryptography and Data Security. FC: Financial Cryptography and Data Security, LNCS, vol. 15751, 307–323.","mla":"Neiheiser, Ray, and Eleftherios Kokoris Kogias. “Anthemius: Efficient and Modular Block Assembly for Concurrent Execution.” <i>29th International Conference on Financial Cryptography and Data Security</i>, vol. 15751, Springer Nature, 2026, pp. 307–23, doi:<a href=\"https://doi.org/10.1007/978-3-032-07024-1_18\">10.1007/978-3-032-07024-1_18</a>.","ieee":"R. Neiheiser and E. Kokoris Kogias, “Anthemius: Efficient and modular block assembly for concurrent execution,” in <i>29th International Conference on Financial Cryptography and Data Security</i>, Miyakojima, Japan, 2026, vol. 15751, pp. 307–323.","chicago":"Neiheiser, Ray, and Eleftherios Kokoris Kogias. “Anthemius: Efficient and Modular Block Assembly for Concurrent Execution.” In <i>29th International Conference on Financial Cryptography and Data Security</i>, 15751:307–23. Springer Nature, 2026. <a href=\"https://doi.org/10.1007/978-3-032-07024-1_18\">https://doi.org/10.1007/978-3-032-07024-1_18</a>."},"title":"Anthemius: Efficient and modular block assembly for concurrent execution","department":[{"_id":"KrPi"}],"quality_controlled":"1","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2502.10074","open_access":"1"}],"date_created":"2026-01-25T23:01:40Z","month":"01","alternative_title":["LNCS"],"oa":1,"scopus_import":"1","publication_status":"published","acknowledgement":"This work was supported by the Austrian Science Fund (FWF) SFB project SpyCoDe F8502 and the Vienna Science and Technology Fund (WWTF) project SCALE2 CT22-045.","external_id":{"arxiv":["2502.10074"]},"arxiv":1,"year":"2026","intvolume":"     15751"},{"volume":44,"doi":"10.1145/3769423","article_processing_charge":"Yes (via OA deal)","OA_type":"hybrid","language":[{"iso":"eng"}],"date_published":"2026-05-01T00:00:00Z","file_date_updated":"2026-07-23T10:04:06Z","issue":"2","publication":"ACM Transactions on Computer Systems","file":[{"success":1,"checksum":"b64822f3d2bcac3c68c887ced45a6008","date_created":"2026-07-23T10:04:06Z","relation":"main_file","file_size":676867,"creator":"dernst","access_level":"open_access","file_name":"2026_TransCompSyst_Neiheiser.pdf","date_updated":"2026-07-23T10:04:06Z","file_id":"22392","content_type":"application/pdf"}],"supplementarymaterial":"no","corr_author":"1","abstract":[{"text":"With the growing interest in blockchains, permissioned approaches to consensus have received increasing attention. Unfortunately, the BFT consensus algorithms that are the backbone of most of these blockchains scale poorly and offer limited throughput. In fact, many state-of-the-art BFT consensus algorithms require a single leader process to receive and validate votes from a quorum of processes and then broadcast the result, which is inherently non-scalable. Recent approaches avoid this bottleneck by using dissemination/aggregation trees to propagate values and collect and validate votes. However, the use of trees increases the round latency, which limits the throughput for deeper trees. In this paper we propose Kauri, a BFT communication abstraction that sustains high throughput as the system size grows by leveraging a novel pipelining technique to perform scalable dissemination and aggregation on trees. Furthermore, when the number of faults is moderate (arguably the most common case in practice), our construction is able to recover from faults in an optimal number of reconfiguration steps. We implemented and experimentally evaluated Kauri with up to 800 processes. Our results show that Kauri outperforms the throughput of state-of-the-art permissioned blockchain protocols, by up to 58x without compromising latency. Interestingly, in some cases, the parallelization provided by Kauri can also decrease the latency.","lang":"eng"}],"status":"public","oa_version":"Published Version","type":"journal_article","publisher":"Association for Computing Machinery","author":[{"orcid":"0000-0001-7227-8309","first_name":"Ray","id":"f09651b9-fec0-11ec-b5d8-934aff0e52a4","full_name":"Neiheiser, Ray","last_name":"Neiheiser"},{"first_name":"Miguel","full_name":"Matos, Miguel","last_name":"Matos"},{"first_name":"Luis","last_name":"Rodrigues","full_name":"Rodrigues, Luis"}],"day":"01","project":[{"name":"Interface Theory for Security and Privacy","grant_number":"F8502","_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e"},{"_id":"7bdd2f70-9f16-11ee-852c-b7950bc6d277","grant_number":"ICT22-045","name":"SeCure, privAte, and interoperabLe layEr 2"}],"date_updated":"2026-07-23T10:07:17Z","keyword":["Distributed systems","byzantine fault tolerance","blockchain","vote aggregation","pipelining"],"intvolume":"        44","das_tickbox":"0","year":"2026","license":"https://creativecommons.org/licenses/by/4.0/","article_type":"original","scopus_import":"1","oa":1,"ddc":["000"],"acknowledgement":"We thank the ACM TOCS Editors and the reviewers for their help in improving the manuscript. This work was partially supported by CAPES - Brazil (Coordenação de Aperfeiçoamento de Pessoal de Nível Superior) and byFundação para a Ciência e Tecnologia (FCT) under project UIDB/50021/2020 and grant 2020.05270.BD, and via project COSMOS (via the OE with ref. PTDC/EEI-COM/29271/2017, via the łPrograma Operacional Regional de Lisboa na sua componente FEDER” with ref. Lisboa-01-0145-FEDER-029271) and project Angainor with reference LISBOA-01-0145-FEDER-031456, grant agreement number 952226, and project GLOG, with reference LISBOA2030-FEDER-00771200, and project BIG (Enhancing the research and innovation potential of Tecnico through blockchain technologies and design Innovation for social Good), and project ScalableCosmosConsensus, and the Austrian Science Fund (FWF) SFB project SpyCoDe F8502 and the Vienna Science and Technology Fund (WWTF) project SCALE2 CT22-045","publication_status":"published","month":"05","title":"Kauri: BFT consensus with pipelined tree-based dissemination and aggregation","department":[{"_id":"KrPi"}],"quality_controlled":"1","date_created":"2026-01-20T10:14:23Z","researchdata_availability":"no","citation":{"chicago":"Neiheiser, Ray, Miguel Matos, and Luis Rodrigues. “Kauri: BFT Consensus with Pipelined Tree-Based Dissemination and Aggregation.” <i>ACM Transactions on Computer Systems</i>. Association for Computing Machinery, 2026. <a href=\"https://doi.org/10.1145/3769423\">https://doi.org/10.1145/3769423</a>.","ieee":"R. Neiheiser, M. Matos, and L. Rodrigues, “Kauri: BFT consensus with pipelined tree-based dissemination and aggregation,” <i>ACM Transactions on Computer Systems</i>, vol. 44, no. 2. Association for Computing Machinery, 2026.","mla":"Neiheiser, Ray, et al. “Kauri: BFT Consensus with Pipelined Tree-Based Dissemination and Aggregation.” <i>ACM Transactions on Computer Systems</i>, vol. 44, no. 2, 12, Association for Computing Machinery, 2026, doi:<a href=\"https://doi.org/10.1145/3769423\">10.1145/3769423</a>.","ista":"Neiheiser R, Matos M, Rodrigues L. 2026. Kauri: BFT consensus with pipelined tree-based dissemination and aggregation. ACM Transactions on Computer Systems. 44(2), 12.","short":"R. Neiheiser, M. Matos, L. Rodrigues, ACM Transactions on Computer Systems 44 (2026).","ama":"Neiheiser R, Matos M, Rodrigues L. Kauri: BFT consensus with pipelined tree-based dissemination and aggregation. <i>ACM Transactions on Computer Systems</i>. 2026;44(2). doi:<a href=\"https://doi.org/10.1145/3769423\">10.1145/3769423</a>","apa":"Neiheiser, R., Matos, M., &#38; Rodrigues, L. (2026). Kauri: BFT consensus with pipelined tree-based dissemination and aggregation. <i>ACM Transactions on Computer Systems</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3769423\">https://doi.org/10.1145/3769423</a>"},"has_accepted_license":"1","PlanS_conform":"1","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"article_number":"12","publication_identifier":{"eissn":["1557-7333"],"issn":["0734-2071"]},"OA_place":"publisher","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"21017"},{"OA_place":"publisher","publication_identifier":{"eissn":["1432-0525"],"issn":["0001-5903"]},"ec_funded":1,"article_number":"43","_id":"20866","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_created":"2025-12-29T12:07:12Z","title":"Hypernode automata","department":[{"_id":"ToHe"}],"quality_controlled":"1","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"citation":{"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>.","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.","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>","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>","ista":"Bartocci E, Chalupa M, Henzinger TA, Nickovic D, Oliveira da Costa A. 2025. Hypernode automata. Acta Informatica. 62(4), 43.","short":"E. Bartocci, M. Chalupa, T.A. Henzinger, D. Nickovic, A. Oliveira da Costa, Acta Informatica 62 (2025)."},"has_accepted_license":"1","ddc":["000"],"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).","publication_status":"published","scopus_import":"1","oa":1,"article_type":"original","month":"12","intvolume":"        62","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"14405"}]},"arxiv":1,"external_id":{"arxiv":["2305.02836"]},"year":"2025","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"},{"grant_number":"F8502","name":"Interface Theory for Security and Privacy","_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e"}],"day":"09","date_updated":"2026-01-05T12:27:41Z","type":"journal_article","author":[{"first_name":"Ezio","full_name":"Bartocci, Ezio","last_name":"Bartocci"},{"id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","first_name":"Marek","full_name":"Chalupa, Marek","last_name":"Chalupa"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"last_name":"Nickovic","full_name":"Nickovic, Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","first_name":"Dejan"},{"id":"f347ec37-6676-11ee-b395-a888cb7b4fb4","first_name":"Ana","orcid":"0000-0002-8741-5799","last_name":"Oliveira da Costa","full_name":"Oliveira da Costa, Ana"}],"publisher":"Springer Nature","corr_author":"1","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."}],"status":"public","issue":"4","publication":"Acta Informatica","file":[{"success":1,"relation":"main_file","date_created":"2026-01-05T12:26:43Z","checksum":"06ed45a1218ad8464818803ae2968aaf","date_updated":"2026-01-05T12:26:43Z","file_name":"2025_ActaInformatica_Bartocci.pdf","file_id":"20944","access_level":"open_access","file_size":7117003,"creator":"dernst","content_type":"application/pdf"}],"oa_version":"Published Version","article_processing_charge":"Yes (via OA deal)","doi":"10.1007/s00236-025-00509-8","volume":62,"date_published":"2025-12-09T00:00:00Z","OA_type":"hybrid","language":[{"iso":"eng"}],"file_date_updated":"2026-01-05T12:26:43Z"},{"scopus_import":"1","oa":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.","publication_status":"published","ddc":["000"],"month":"11","related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"21401"}]},"arxiv":1,"external_id":{"arxiv":["2505.09276"]},"year":"2025","ec_funded":1,"OA_place":"publisher","publication_identifier":{"isbn":["9798400715259"]},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"21020","title":"Privacy-preserving runtime verification","department":[{"_id":"ToHe"},{"_id":"GradSch"}],"quality_controlled":"1","date_created":"2026-01-20T10:17:10Z","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>.","ieee":"T. A. Henzinger, M. Karimi, and K. S. Thejaswini, “Privacy-preserving runtime verification,” in <i>Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security</i>, Taipei, Taiwan, 2025, pp. 2774–2787.","chicago":"Henzinger, Thomas A, Mahyar Karimi, and K. S. Thejaswini. “Privacy-Preserving Runtime Verification.” In <i>Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security</i>, 2774–87. Association for Computing Machinery, 2025. <a href=\"https://doi.org/10.1145/3719027.3765137\">https://doi.org/10.1145/3719027.3765137</a>.","apa":"Henzinger, T. A., Karimi, M., &#38; Thejaswini, K. S. (2025). Privacy-preserving runtime verification. In <i>Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security</i> (pp. 2774–2787). Taipei, Taiwan: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3719027.3765137\">https://doi.org/10.1145/3719027.3765137</a>","ama":"Henzinger TA, Karimi M, Thejaswini KS. Privacy-preserving runtime verification. In: <i>Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security</i>. Association for Computing Machinery; 2025:2774-2787. doi:<a href=\"https://doi.org/10.1145/3719027.3765137\">10.1145/3719027.3765137</a>","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.","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."},"has_accepted_license":"1","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"publication":"Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security","file":[{"success":1,"checksum":"615ffddab6c7285158c2953acec6fa6f","date_created":"2026-01-21T07:34:58Z","relation":"main_file","file_size":1241912,"creator":"dernst","access_level":"open_access","date_updated":"2026-01-21T07:34:58Z","file_id":"21024","file_name":"2025_CCS_HenzingerT.pdf","content_type":"application/pdf"}],"corr_author":"1","abstract":[{"text":"Runtime verification offers scalable solutions to improve the safety and reliability of systems. However, systems that require verification or monitoring by a third party to ensure compliance with a specification might contain sensitive information, causing privacy concerns when usual runtime verification approaches are used. Privacy is compromised if protected information about the system, or sensitive data that is processed by the system, is revealed. In addition, revealing the specification being monitored may undermine the essence of third-party verification.\r\nIn this work, we propose two novel protocols for the privacy-preserving runtime verification of systems against formal sequential specifications. In our first protocol, the monitor verifies whether the system satisfies the specification without learning anything else, though both parties are aware of the specification. Our second protocol ensures that the system remains oblivious to the monitored specification, while the monitor learns only whether the system satisfies the specification and nothing more. Our protocols adapt and improve existing techniques used in cryptography, and more specifically, multi-party computation.\r\nThe sequential specification defines the observation step of the monitor, whose granularity depends on the situation (e.g., banks may be monitored on a daily basis). Our protocols exchange a single message per observation step, after an initialisation phase. This design minimises communication overhead, enabling relatively lightweight privacy-preserving monitoring. We implement our approach for monitoring specifications described by register automata and evaluate it experimentally.","lang":"eng"}],"status":"public","oa_version":"Published Version","conference":{"end_date":"2025-10-17","name":"CCS: Conference on Computer and Communications Security","start_date":"2025-10-13","location":"Taipei, Taiwan"},"page":"2774-2787","doi":"10.1145/3719027.3765137","article_processing_charge":"Yes (via OA deal)","date_published":"2025-11-22T00:00:00Z","language":[{"iso":"eng"}],"OA_type":"hybrid","file_date_updated":"2026-01-21T07:34:58Z","day":"22","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"},{"_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e","grant_number":"F8502","name":"Interface Theory for Security and Privacy"}],"date_updated":"2026-03-13T13:37:19Z","type":"conference","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"id":"6e5417ba-5355-11ee-ae5a-94c2e510b26b","first_name":"Mahyar","orcid":"0009-0005-0820-1696","full_name":"Karimi, Mahyar","last_name":"Karimi"},{"last_name":"Thejaswini","full_name":"Thejaswini, K. S.","first_name":"K. S.","id":"3807fb92-fdc1-11ee-bb4a-b4d8a431c753"}],"publisher":"Association for Computing Machinery"},{"volume":360,"page":"20:1-20:18","article_processing_charge":"No","doi":"10.4230/LIPICS.FSTTCS.2025.20","date_published":"2025-12-09T00:00:00Z","language":[{"iso":"eng"}],"OA_type":"gold","file_date_updated":"2026-02-11T09:33:20Z","publication":"45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science","file":[{"relation":"main_file","checksum":"8188ee5c7b14193d48eeb655e9bbdc47","date_created":"2026-02-11T09:33:20Z","success":1,"content_type":"application/pdf","file_size":933970,"creator":"dernst","file_name":"2025_LIPIcS_Chalupa.pdf","date_updated":"2026-02-11T09:33:20Z","file_id":"21213","access_level":"open_access"}],"abstract":[{"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.","lang":"eng"}],"corr_author":"1","status":"public","oa_version":"Published Version","conference":{"end_date":"2025-12-19","location":"Pilani, India","start_date":"2025-12-17","name":"FSTTCS: Conference on Foundations of Software Technology and Theoretical Computer Science"},"type":"conference","author":[{"id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","first_name":"Marek","full_name":"Chalupa, Marek","last_name":"Chalupa"},{"orcid":"0000-0002-2985-7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"id":"8b282559-50b0-11ef-861e-d6ace0d92e9b","first_name":"Ana A","last_name":"Oliveira da Costa","full_name":"Oliveira da Costa, Ana A"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","day":"09","project":[{"_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e","name":"Interface Theory for Security and Privacy","grant_number":"F8502"},{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}],"date_updated":"2026-02-11T09:35:04Z","intvolume":"       360","external_id":{"arxiv":["2510.12298"]},"arxiv":1,"year":"2025","alternative_title":["LIPIcs"],"oa":1,"scopus_import":"1","publication_status":"published","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.","ddc":["000"],"month":"12","title":"Flavors of quantifiers in hyperlogics","department":[{"_id":"ToHe"}],"quality_controlled":"1","date_created":"2026-01-29T15:39:15Z","citation":{"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>.","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.","mla":"Chalupa, Marek, et al. “Flavors of Quantifiers in Hyperlogics.” <i>45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>, vol. 360, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025, p. 20:1-20:18, doi:<a href=\"https://doi.org/10.4230/LIPICS.FSTTCS.2025.20\">10.4230/LIPICS.FSTTCS.2025.20</a>.","ista":"Chalupa M, Henzinger TA, Oliveira da Costa AA. 2025. Flavors of quantifiers in hyperlogics. 45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science. FSTTCS: Conference on Foundations of Software Technology and Theoretical Computer Science, LIPIcs, vol. 360, 20:1-20:18.","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.","apa":"Chalupa, M., Henzinger, T. A., &#38; Oliveira da Costa, A. A. (2025). Flavors of quantifiers in hyperlogics. In <i>45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i> (Vol. 360, p. 20:1-20:18). Pilani, India: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPICS.FSTTCS.2025.20\">https://doi.org/10.4230/LIPICS.FSTTCS.2025.20</a>","ama":"Chalupa M, Henzinger TA, Oliveira da Costa AA. Flavors of quantifiers in hyperlogics. In: <i>45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science</i>. Vol 360. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2025:20:1-20:18. doi:<a href=\"https://doi.org/10.4230/LIPICS.FSTTCS.2025.20\">10.4230/LIPICS.FSTTCS.2025.20</a>"},"has_accepted_license":"1","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"ec_funded":1,"OA_place":"publisher","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"21089"},{"date_published":"2025-09-13T00:00:00Z","OA_type":"green","language":[{"iso":"eng"}],"volume":16087,"page":"417-437","doi":"10.1007/978-3-032-05435-7_23","article_processing_charge":"No","oa_version":"Preprint","conference":{"name":"RV: Runtime Verification","start_date":"2025-09-15","location":"Graz, Austria","end_date":"2025-09-19"},"publication":"25th International Conference on Runtime Verification","corr_author":"1","abstract":[{"text":"We propose a monitoring approach for hyperproperties where the system’s observations range over infinite domains. The specifications are given as formulas of symbolic hypernode logic, an extension of earlier versions of hypernode logic that supports events with data. We demonstrate how to translate terms of symbolic hypernode logic into multi-tape symbolic transducers and we present a monitoring algorithm for universally quantified formulas that is based on this translation. We evaluate our approach against the previous approach for monitoring hypernode logic, and we also compare it to other monitors for hyperproperties.","lang":"eng"}],"status":"public","publisher":"Springer Nature","author":[{"last_name":"Chalupa","full_name":"Chalupa, Marek","first_name":"Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"8b282559-50b0-11ef-861e-d6ace0d92e9b","first_name":"Ana A","full_name":"Oliveira da Costa, Ana A","last_name":"Oliveira da Costa"}],"type":"conference","date_updated":"2026-02-16T11:59:20Z","day":"13","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"},{"_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e","name":"Interface Theory for Security and Privacy","grant_number":"F8502"}],"arxiv":1,"external_id":{"arxiv":["2508.02301"]},"year":"2025","intvolume":"     16087","month":"09","alternative_title":["LNCS"],"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).","citation":{"ama":"Chalupa M, Henzinger TA, Oliveira da Costa AA. Monitoring hypernode logic over infinite domains. In: <i>25th International Conference on Runtime Verification</i>. Vol 16087. Springer Nature; 2025:417-437. doi:<a href=\"https://doi.org/10.1007/978-3-032-05435-7_23\">10.1007/978-3-032-05435-7_23</a>","apa":"Chalupa, M., Henzinger, T. A., &#38; Oliveira da Costa, A. A. (2025). Monitoring hypernode logic over infinite domains. In <i>25th International Conference on Runtime Verification</i> (Vol. 16087, pp. 417–437). Graz, Austria: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-032-05435-7_23\">https://doi.org/10.1007/978-3-032-05435-7_23</a>","short":"M. Chalupa, T.A. Henzinger, A.A. Oliveira da Costa, in:, 25th International Conference on Runtime Verification, Springer Nature, 2025, pp. 417–437.","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.","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>.","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.","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>."},"title":"Monitoring hypernode logic over infinite domains","quality_controlled":"1","department":[{"_id":"ToHe"}],"main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2508.02301","open_access":"1"}],"date_created":"2026-01-29T16:04:31Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"21093","ec_funded":1,"OA_place":"repository","publication_identifier":{"eisbn":["9783032054357"],"issn":["0302-9743"],"eissn":["1611-3349"]}},{"publication_status":"published","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].","ddc":["000"],"scopus_import":"1","oa":1,"article_type":"original","month":"05","intvolume":"        66","related_material":{"record":[{"id":"11355","relation":"shorter_version","status":"public"}]},"arxiv":1,"external_id":{"arxiv":["2002.06465"],"isi":["001230084200001"]},"year":"2025","publication_identifier":{"eissn":["1572-8102"],"issn":["0925-9856"]},"OA_place":"publisher","ec_funded":1,"_id":"17094","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_created":"2024-06-02T22:00:57Z","title":"Information-flow interfaces","quality_controlled":"1","department":[{"_id":"ToHe"}],"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"PlanS_conform":"1","citation":{"mla":"Bartocci, Ezio, et al. “Information-Flow Interfaces.” <i>Formal Methods in System Design</i>, vol. 66, Springer Nature, 2025, pp. 3–48, doi:<a href=\"https://doi.org/10.1007/s10703-024-00447-0\">10.1007/s10703-024-00447-0</a>.","chicago":"Bartocci, Ezio, Thomas Ferrere, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira da Costa. “Information-Flow Interfaces.” <i>Formal Methods in System Design</i>. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/s10703-024-00447-0\">https://doi.org/10.1007/s10703-024-00447-0</a>.","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.","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>","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.","short":"E. Bartocci, T. Ferrere, T.A. Henzinger, D. Nickovic, A. Oliveira da Costa, Formal Methods in System Design 66 (2025) 3–48."},"has_accepted_license":"1","abstract":[{"text":"Contract-based design is a promising methodology for taming the complexity of developing sophisticated systems. A formal contract distinguishes between assumptions, which are constraints that the designer of a component puts on the environments in which the component can be used safely, and guarantees, which are promises that the designer asks from the team that implements the component. A theory of formal contracts can be formalized as an interface theory, which supports the composition and refinement of both assumptions and guarantees. Although there is a rich landscape of contract-based design methods that address functional and extra-functional properties, we present the first interface theory designed to ensure system-wide security properties. Our framework provides a refinement relation and a composition operation that support both incremental design and independent implementability. We develop our theory for both stateless and stateful interfaces. Additionally, we introduce information-flow contracts where assumptions and guarantees are sets of flow relations. We use these contracts to illustrate how to enrich information-flow interfaces with a semantic view. We illustrate the applicability of our framework with two examples inspired by the automotive domain.","lang":"eng"}],"corr_author":"1","status":"public","file":[{"content_type":"application/pdf","creator":"dernst","file_size":3860690,"access_level":"open_access","file_name":"2025_FormalMethodsSysDesign_Bartocci.pdf","date_updated":"2025-12-30T06:50:12Z","file_id":"20879","date_created":"2025-12-30T06:50:12Z","checksum":"244a71a916103b8ea08e9d0bab32bcd9","relation":"main_file","success":1}],"publication":"Formal Methods in System Design","oa_version":"Published Version","page":"3-48","doi":"10.1007/s10703-024-00447-0","article_processing_charge":"Yes (via OA deal)","volume":66,"language":[{"iso":"eng"}],"OA_type":"hybrid","date_published":"2025-05-01T00:00:00Z","file_date_updated":"2025-12-30T06:50:12Z","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"},{"_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e","grant_number":"F8502","name":"Interface Theory for Security and Privacy"}],"isi":1,"day":"01","date_updated":"2025-12-30T06:50:51Z","type":"journal_article","publisher":"Springer Nature","author":[{"first_name":"Ezio","full_name":"Bartocci, Ezio","last_name":"Bartocci"},{"id":"40960E6E-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas","orcid":"0000-0001-5199-3143","full_name":"Ferrere, Thomas","last_name":"Ferrere"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"last_name":"Nickovic","full_name":"Nickovic, Dejan","first_name":"Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-8741-5799","id":"f347ec37-6676-11ee-b395-a888cb7b4fb4","first_name":"Ana","full_name":"Oliveira da Costa, Ana","last_name":"Oliveira da Costa"}]},{"acknowledgement":"This project was funded in part by the Austrian Science Fund (FWF) SFB project SpyCoDe F8502, Vienna Science and Technology Fund (WWTF) [10.47379/ICT19018] (ProbInG) and WWTF project ICT22-023 (TAIGER), National Science Foundation (NSF) CPS Award 1837680, NSF award ECCS-2144416 and NSF SaTC Award 2245114. Open access funding provided by Institute of Science and Technology (IST Austria).","publication_status":"published","ddc":["000"],"oa":1,"scopus_import":"1","article_type":"original","month":"09","intvolume":"        62","year":"2025","external_id":{"isi":["001546115300001"]},"publication_identifier":{"issn":["0001-5903"],"eissn":["1432-0525"]},"OA_place":"publisher","article_number":"30","_id":"20186","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_created":"2025-08-17T22:01:36Z","department":[{"_id":"ToHe"}],"quality_controlled":"1","title":"Gray-box runtime enforcement of hyperproperties","PlanS_conform":"1","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)"},"has_accepted_license":"1","citation":{"mla":"Hsu, Tzu Han, et al. “Gray-Box Runtime Enforcement of Hyperproperties.” <i>Acta Informatica</i>, vol. 62, no. 3, 30, Springer Nature, 2025, doi:<a href=\"https://doi.org/10.1007/s00236-025-00502-1\">10.1007/s00236-025-00502-1</a>.","chicago":"Hsu, Tzu Han, Ana A Oliveira da Costa, Andrew Wintenberg, Ezio Bartocci, and Borzoo Bonakdarpour. “Gray-Box Runtime Enforcement of Hyperproperties.” <i>Acta Informatica</i>. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/s00236-025-00502-1\">https://doi.org/10.1007/s00236-025-00502-1</a>.","ieee":"T. H. Hsu, A. A. Oliveira da Costa, A. Wintenberg, E. Bartocci, and B. Bonakdarpour, “Gray-box runtime enforcement of hyperproperties,” <i>Acta Informatica</i>, vol. 62, no. 3. Springer Nature, 2025.","apa":"Hsu, T. H., Oliveira da Costa, A. A., Wintenberg, A., Bartocci, E., &#38; Bonakdarpour, B. (2025). Gray-box runtime enforcement of hyperproperties. <i>Acta Informatica</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s00236-025-00502-1\">https://doi.org/10.1007/s00236-025-00502-1</a>","ama":"Hsu TH, Oliveira da Costa AA, Wintenberg A, Bartocci E, Bonakdarpour B. Gray-box runtime enforcement of hyperproperties. <i>Acta Informatica</i>. 2025;62(3). doi:<a href=\"https://doi.org/10.1007/s00236-025-00502-1\">10.1007/s00236-025-00502-1</a>","ista":"Hsu TH, Oliveira da Costa AA, Wintenberg A, Bartocci E, Bonakdarpour B. 2025. Gray-box runtime enforcement of hyperproperties. Acta Informatica. 62(3), 30.","short":"T.H. Hsu, A.A. Oliveira da Costa, A. Wintenberg, E. Bartocci, B. Bonakdarpour, Acta Informatica 62 (2025)."},"status":"public","corr_author":"1","abstract":[{"lang":"eng","text":"Enforcement of information-flow policies has been extensively studied by language-based approaches over the past few decades. In this paper, we propose an alternative, novel, general, and effective approach using enforcement of hyperproperties– a powerful formalism for expressing and reasoning about a wide range of information-flow security policies. We study black- vs. gray- vs. white-box enforcement of hyperproperties expressed by nondeterministic finite-word hyperautomata (NFH), where the enforcer has null, some, or complete information about the implementation of the system under scrutiny. Given an NFH, in order to generate a runtime enforcer, we reduce the problem to controller synthesis for hyperproperties and subsequently to the satisfiability problem for quantified Boolean formulas (QBFs). The resulting enforcers are transferable with low-overhead. We conduct a rich set of case studies, including information-flow control for JavaScript code, as well as synthesizing obfuscators for control plants."}],"file":[{"file_id":"20267","file_name":"2025_ActaInformatica_Hsu.pdf","date_updated":"2025-09-02T05:53:47Z","access_level":"open_access","file_size":6505049,"creator":"dernst","content_type":"application/pdf","success":1,"relation":"main_file","checksum":"90a43350fd4a8c5cb5b1b0e1aea7970d","date_created":"2025-09-02T05:53:47Z"}],"publication":"Acta Informatica","issue":"3","oa_version":"Published Version","doi":"10.1007/s00236-025-00502-1","article_processing_charge":"Yes (via OA deal)","volume":62,"file_date_updated":"2025-09-02T05:53:47Z","OA_type":"hybrid","date_published":"2025-09-01T00:00:00Z","language":[{"iso":"eng"}],"project":[{"_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e","name":"Interface Theory for Security and Privacy","grant_number":"F8502"}],"isi":1,"day":"01","date_updated":"2025-09-30T14:20:11Z","type":"journal_article","publisher":"Springer Nature","author":[{"last_name":"Hsu","full_name":"Hsu, Tzu Han","first_name":"Tzu Han"},{"first_name":"Ana A","id":"8b282559-50b0-11ef-861e-d6ace0d92e9b","full_name":"Oliveira Da Costa, Ana A","last_name":"Oliveira Da Costa"},{"full_name":"Wintenberg, Andrew","last_name":"Wintenberg","first_name":"Andrew"},{"first_name":"Ezio","last_name":"Bartocci","full_name":"Bartocci, Ezio"},{"full_name":"Bonakdarpour, Borzoo","last_name":"Bonakdarpour","first_name":"Borzoo"}]},{"_id":"20723","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","OA_place":"repository","publication_identifier":{"eissn":["1611-3349"],"isbn":["9783031975363"],"issn":["0302-9743"],"eisbn":["9783031975370"]},"ec_funded":1,"citation":{"ieee":"E. Bartocci, T. A. Henzinger, D. Nickovic, and A. Oliveira da Costa, “Information-Flow Interfaces and Security Lattices,” in <i>Engineering Safe and Trustworthy Cyber Physical Systems</i>, vol. 15471, Cham: Springer Nature, 2025, pp. 251–263.","chicago":"Bartocci, Ezio, Thomas A Henzinger, Dejan Nickovic, and Ana Oliveira da Costa. “Information-Flow Interfaces and Security Lattices.” In <i>Engineering Safe and Trustworthy Cyber Physical Systems</i>, 15471:251–63. Cham: Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-97537-0_15\">https://doi.org/10.1007/978-3-031-97537-0_15</a>.","mla":"Bartocci, Ezio, et al. “Information-Flow Interfaces and Security Lattices.” <i>Engineering Safe and Trustworthy Cyber Physical Systems</i>, vol. 15471, Springer Nature, 2025, pp. 251–63, doi:<a href=\"https://doi.org/10.1007/978-3-031-97537-0_15\">10.1007/978-3-031-97537-0_15</a>.","short":"E. Bartocci, T.A. Henzinger, D. Nickovic, A. Oliveira da Costa, in:, Engineering Safe and Trustworthy Cyber Physical Systems, Springer Nature, Cham, 2025, pp. 251–263.","ista":"Bartocci E, Henzinger TA, Nickovic D, Oliveira da Costa A. 2025.Information-Flow Interfaces and Security Lattices. In: Engineering Safe and Trustworthy Cyber Physical Systems. LNCS, vol. 15471, 251–263.","ama":"Bartocci E, Henzinger TA, Nickovic D, Oliveira da Costa A. Information-Flow Interfaces and Security Lattices. In: <i>Engineering Safe and Trustworthy Cyber Physical Systems</i>. Vol 15471. Cham: Springer Nature; 2025:251-263. doi:<a href=\"https://doi.org/10.1007/978-3-031-97537-0_15\">10.1007/978-3-031-97537-0_15</a>","apa":"Bartocci, E., Henzinger, T. A., Nickovic, D., &#38; Oliveira da Costa, A. (2025). Information-Flow Interfaces and Security Lattices. In <i>Engineering Safe and Trustworthy Cyber Physical Systems</i> (Vol. 15471, pp. 251–263). Cham: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-97537-0_15\">https://doi.org/10.1007/978-3-031-97537-0_15</a>"},"date_created":"2025-12-01T15:44:58Z","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2406.14374"}],"quality_controlled":"1","department":[{"_id":"ToHe"}],"title":"Information-Flow Interfaces and Security Lattices","month":"10","publication_status":"published","acknowledgement":"This project was funded in part by the Austrian Science Fund (FWF) SFB project SpyCoDe F8502 and by the ERC-2020-AdG 101020093.","scopus_import":"1","oa":1,"alternative_title":["LNCS"],"year":"2025","arxiv":1,"external_id":{"arxiv":["2406.14374"]},"intvolume":"     15471","date_updated":"2025-12-09T07:57:55Z","place":"Cham","project":[{"_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e","grant_number":"F8502","name":"Interface Theory for Security and Privacy"},{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"day":"02","publisher":"Springer Nature","author":[{"last_name":"Bartocci","full_name":"Bartocci, Ezio","first_name":"Ezio"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000-0002-2985-7724"},{"first_name":"Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","last_name":"Nickovic","full_name":"Nickovic, Dejan"},{"orcid":"0000-0002-8741-5799","first_name":"Ana","id":"f347ec37-6676-11ee-b395-a888cb7b4fb4","full_name":"Oliveira da Costa, Ana","last_name":"Oliveira da Costa"}],"type":"book_chapter","oa_version":"Preprint","status":"public","corr_author":"1","abstract":[{"text":"Information-flow interfaces is a formalism recently proposed for specifying, composing, and refining system-wide security requirements. In this work, we show how the widely used concept of security lattices provides a natural semantic interpretation for information-flow interfaces.","lang":"eng"}],"publication":"Engineering Safe and Trustworthy Cyber Physical Systems","date_published":"2025-10-02T00:00:00Z","language":[{"iso":"eng"}],"OA_type":"green","doi":"10.1007/978-3-031-97537-0_15","article_processing_charge":"No","page":"251-263","volume":15471},{"type":"conference","publisher":"Springer Nature","author":[{"full_name":"Chalupa, Marek","last_name":"Chalupa","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","first_name":"Marek"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"orcid":"0000-0002-8741-5799","first_name":"Ana","id":"f347ec37-6676-11ee-b395-a888cb7b4fb4","last_name":"Oliveira da Costa","full_name":"Oliveira da Costa, Ana"}],"day":"13","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"},{"_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e","name":"Interface Theory for Security and Privacy","grant_number":"F8502"}],"isi":1,"date_updated":"2025-09-08T14:47:22Z","volume":15234,"page":"151-171","article_processing_charge":"No","doi":"10.1007/978-3-031-76554-4_9","OA_type":"closed access","language":[{"iso":"eng"}],"date_published":"2024-11-13T00:00:00Z","publication":"Integrated Formal Methods","corr_author":"1","abstract":[{"lang":"eng","text":"Hypernode logic can reason about the prefix relation on stutter-reduced finite traces through the stutter-reduced prefix predicate. We increase the expressiveness of hypernode logic in two ways. First, we split the stutter-reduced prefix predicate into an explicit stutter-reduction operator and the classical prefix predicate on words. This change gives hypernode logic the ability to combine synchronous and asynchronous reasoning by explicitly stating which parts of traces can stutter. Second, we allow the use of regular expressions in formulas to reason about the structure of traces. This change enables hypernode logic to describe a mixture of trace properties and hyperproperties.\r\n\r\nWe show how to translate extended hypernode logic formulas into multi-track automata, which are automata that read multiple input words. Then we describe a fully online monitoring algorithm for monitoring k-safety hyperproperties specified in the logic. We have implemented the monitoring algorithm, and evaluated it on monitoring synchronous and asynchronous versions of observational determinism, and on checking the privacy preservation by compiler optimizations."}],"status":"public","oa_version":"None","title":"Monitoring extended hypernode logic","department":[{"_id":"ToHe"}],"quality_controlled":"1","date_created":"2024-12-01T23:01:52Z","citation":{"mla":"Chalupa, Marek, et al. “Monitoring Extended Hypernode Logic.” <i>Integrated Formal Methods</i>, vol. 15234, Springer Nature, 2024, pp. 151–71, doi:<a href=\"https://doi.org/10.1007/978-3-031-76554-4_9\">10.1007/978-3-031-76554-4_9</a>.","chicago":"Chalupa, Marek, Thomas A Henzinger, and Ana Oliveira da Costa. “Monitoring Extended Hypernode Logic.” In <i>Integrated Formal Methods</i>, 15234:151–71. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-76554-4_9\">https://doi.org/10.1007/978-3-031-76554-4_9</a>.","ieee":"M. Chalupa, T. A. Henzinger, and A. Oliveira da Costa, “Monitoring extended hypernode logic,” in <i>Integrated Formal Methods</i>, 2024, vol. 15234, pp. 151–171.","apa":"Chalupa, M., Henzinger, T. A., &#38; Oliveira da Costa, A. (2024). Monitoring extended hypernode logic. In <i>Integrated Formal Methods</i> (Vol. 15234, pp. 151–171). Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-76554-4_9\">https://doi.org/10.1007/978-3-031-76554-4_9</a>","ama":"Chalupa M, Henzinger TA, Oliveira da Costa A. Monitoring extended hypernode logic. In: <i>Integrated Formal Methods</i>. Vol 15234. Springer Nature; 2024:151-171. doi:<a href=\"https://doi.org/10.1007/978-3-031-76554-4_9\">10.1007/978-3-031-76554-4_9</a>","ista":"Chalupa M, Henzinger TA, Oliveira da Costa A. 2024. Monitoring extended hypernode logic. Integrated Formal Methods. , LNCS, vol. 15234, 151–171.","short":"M. Chalupa, T.A. Henzinger, A. Oliveira da Costa, in:, Integrated Formal Methods, Springer Nature, 2024, pp. 151–171."},"ec_funded":1,"publication_identifier":{"issn":["0302-9743"],"isbn":["9783031765537"],"eissn":["1611-3349"]},"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","_id":"18599","intvolume":"     15234","external_id":{"isi":["001416640500009"]},"year":"2024","alternative_title":["LNCS"],"scopus_import":"1","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093, and by the Austrian Science Fund (FWF) SFB project SpyCoDe F8502.","publication_status":"published","month":"11"}]