[{"isi":1,"publication":"Science of Computer Programming","date_updated":"2025-09-09T12:25:29Z","file_date_updated":"2025-01-13T09:02:47Z","scopus_import":"1","issue":"2","ec_funded":1,"status":"public","has_accepted_license":"1","citation":{"ista":"Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. 2025. VAMOS: Middleware for best-effort third-party monitoring. Science of Computer Programming. 240(2), 103212.","ama":"Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. VAMOS: Middleware for best-effort third-party monitoring. <i>Science of Computer Programming</i>. 2025;240(2). doi:<a href=\"https://doi.org/10.1016/j.scico.2024.103212\">10.1016/j.scico.2024.103212</a>","chicago":"Chalupa, Marek, Fabian Mühlböck, Stefanie Muroya Lei, and Thomas A Henzinger. “VAMOS: Middleware for Best-Effort Third-Party Monitoring.” <i>Science of Computer Programming</i>. Elsevier, 2025. <a href=\"https://doi.org/10.1016/j.scico.2024.103212\">https://doi.org/10.1016/j.scico.2024.103212</a>.","ieee":"M. Chalupa, F. Mühlböck, S. Muroya Lei, and T. A. Henzinger, “VAMOS: Middleware for best-effort third-party monitoring,” <i>Science of Computer Programming</i>, vol. 240, no. 2. Elsevier, 2025.","short":"M. Chalupa, F. Mühlböck, S. Muroya Lei, T.A. Henzinger, Science of Computer Programming 240 (2025).","mla":"Chalupa, Marek, et al. “VAMOS: Middleware for Best-Effort Third-Party Monitoring.” <i>Science of Computer Programming</i>, vol. 240, no. 2, 103212, Elsevier, 2025, doi:<a href=\"https://doi.org/10.1016/j.scico.2024.103212\">10.1016/j.scico.2024.103212</a>.","apa":"Chalupa, M., Mühlböck, F., Muroya Lei, S., &#38; Henzinger, T. A. (2025). VAMOS: Middleware for best-effort third-party monitoring. <i>Science of Computer Programming</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.scico.2024.103212\">https://doi.org/10.1016/j.scico.2024.103212</a>"},"day":"01","type":"journal_article","quality_controlled":"1","language":[{"iso":"eng"}],"_id":"18169","abstract":[{"lang":"eng","text":"As the complexity and criticality of software increase every year, so does the importance of runtime monitoring. Third-party and best-effort monitoring are especially valuable, yet under-explored areas of runtime monitoring. In this context, third-party monitoring means monitoring with a limited knowledge of the monitored software (as it has been developed by a third party). Best-effort monitoring keeps pace with the monitored software at the cost of possibly imprecise verdicts when keeping up with the monitored software would not be feasible. Most existing monitoring frameworks do not support the combination of third-party and best-effort monitoring because they either require the full access to the monitored code or the ability to process all observable events, or both.\r\nWe present a middleware framework, Vamos, for the runtime monitoring of software. Vamos is explicitly designed to support third-party and best-effort scenarios. The design goals of Vamos are (i) efficiency (tracing events with low overhead), (ii) flexibility (the ability to monitor a variety of different event channels, and to connect to a wide range of monitors), and (iii) ease-of-use. To achieve its goals, Vamos combines aspects of event broker and event recognition systems with aspects of stream processing systems.\r\nWe implemented a prototype toolchain for Vamos and conducted a set of experiments demonstrating the usability of the scheme. The results indicate that Vamos enables writing useful yet efficient monitors, and simplifies key aspects of setting up a monitoring system from scratch."}],"external_id":{"isi":["001327852600001"]},"date_published":"2025-02-01T00:00:00Z","OA_place":"publisher","year":"2025","ddc":["000"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_number":"103212","intvolume":"       240","project":[{"name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}],"article_type":"original","month":"02","department":[{"_id":"ToHe"}],"volume":240,"author":[{"last_name":"Chalupa","full_name":"Chalupa, Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","first_name":"Marek"},{"full_name":"Mühlböck, Fabian","last_name":"Mühlböck","first_name":"Fabian","id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425","orcid":"0000-0003-1548-0177"},{"last_name":"Muroya Lei","full_name":"Muroya Lei, Stefanie","id":"a376de31-8972-11ed-ae7b-d0251c13c8ff","first_name":"Stefanie"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger"}],"acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093. The authors would like to thank the STTT reviewers for their valuable feedback and suggestions.","doi":"10.1016/j.scico.2024.103212","oa":1,"related_material":{"record":[{"relation":"earlier_version","id":"12856","status":"public"}]},"publisher":"Elsevier","corr_author":"1","tmp":{"short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"article_processing_charge":"Yes (via OA deal)","file":[{"relation":"main_file","file_id":"18831","date_updated":"2025-01-13T09:02:47Z","creator":"dernst","file_name":"2024_ScienceCompProg_Chalupa.pdf","checksum":"cd93c0c356e479ffccfbe8499b6ba8e2","file_size":1173677,"date_created":"2025-01-13T09:02:47Z","success":1,"content_type":"application/pdf","access_level":"open_access"}],"publication_status":"published","oa_version":"Published Version","OA_type":"hybrid","title":"VAMOS: Middleware for best-effort third-party monitoring","date_created":"2024-10-06T22:01:10Z","publication_identifier":{"issn":["0167-6423"]}},{"year":"2025","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_published":"2025-05-01T00:00:00Z","language":[{"iso":"eng"}],"_id":"20024","abstract":[{"text":"Cooperative software verification divides the task of software verification among several verification tools in order to increase efficiency and effectiveness. The basic approach is to let verifiers work on different parts of a program and at the end join verification results. While this idea is intuitively appealing, cooperative verification is usually hindered by the fact that program decomposition (1) is often static, disregarding strengths and weaknesses of employed verifiers, and (2) often represents the decomposed program parts in a specific proprietary format, thereby making the use of off-the-shelf verifiers in cooperative verification difficult. In this paper, we propose a novel cooperative verification scheme that we call dynamic program splitting (DPS). Splitting decomposes programs into (smaller) programs, and thus directly enables the use of off-the-shelf tools. In DPS, splitting is dynamically applied on demand: Verification starts by giving a verification task (a program plus a correctness specification) to a verifier V1. Whenever V1 finds the current task to be hard to verify, it splits the task (i.e., the program) and restarts verification on subtasks. DPS continues until (1) a violation is found, (2) all subtasks are completed or (3) some user-defined stopping criterion is met. In the latter case, the remaining uncompleted subtasks are merged into a single one and are given to a next verifier V2, repeating the same procedure on the still unverified program parts. This way, the decomposition is steered by what is hard to verify for particular verifiers, leveraging their complementary strengths. We have implemented dynamic program splitting and evaluated it on benchmarks of the annual software verification competition SV-COMP. The evaluation shows that cooperative verification with DPS is able to solve verification tasks that none of the constituent verifiers can solve, without any significant overhead.","lang":"eng"}],"external_id":{"isi":["001538318100163"]},"type":"conference","quality_controlled":"1","day":"01","citation":{"ama":"Richter C, Chalupa M, Jakobs M-C, Wehrheim H. Cooperative software verification via dynamic program splitting. In: <i>47th International Conference on Software Engineering</i>. IEEE; 2025:2087-2099. doi:<a href=\"https://doi.org/10.1109/ICSE55347.2025.00092\">10.1109/ICSE55347.2025.00092</a>","ista":"Richter C, Chalupa M, Jakobs M-C, Wehrheim H. 2025. Cooperative software verification via dynamic program splitting. 47th International Conference on Software Engineering. ICSE: International Conference on Software Engineering, 2087–2099.","chicago":"Richter, Cedric, Marek Chalupa, Marie-Christine Jakobs, and Heike Wehrheim. “Cooperative Software Verification via Dynamic Program Splitting.” In <i>47th International Conference on Software Engineering</i>, 2087–99. IEEE, 2025. <a href=\"https://doi.org/10.1109/ICSE55347.2025.00092\">https://doi.org/10.1109/ICSE55347.2025.00092</a>.","mla":"Richter, Cedric, et al. “Cooperative Software Verification via Dynamic Program Splitting.” <i>47th International Conference on Software Engineering</i>, IEEE, 2025, pp. 2087–99, doi:<a href=\"https://doi.org/10.1109/ICSE55347.2025.00092\">10.1109/ICSE55347.2025.00092</a>.","short":"C. Richter, M. Chalupa, M.-C. Jakobs, H. Wehrheim, in:, 47th International Conference on Software Engineering, IEEE, 2025, pp. 2087–2099.","ieee":"C. Richter, M. Chalupa, M.-C. Jakobs, and H. Wehrheim, “Cooperative software verification via dynamic program splitting,” in <i>47th International Conference on Software Engineering</i>, Ottawa, ON, Canada, 2025, pp. 2087–2099.","apa":"Richter, C., Chalupa, M., Jakobs, M.-C., &#38; Wehrheim, H. (2025). Cooperative software verification via dynamic program splitting. In <i>47th International Conference on Software Engineering</i> (pp. 2087–2099). Ottawa, ON, Canada: IEEE. <a href=\"https://doi.org/10.1109/ICSE55347.2025.00092\">https://doi.org/10.1109/ICSE55347.2025.00092</a>"},"page":"2087-2099","status":"public","ec_funded":1,"scopus_import":"1","date_updated":"2025-09-30T14:01:55Z","publication":"47th International Conference on Software Engineering","isi":1,"publication_identifier":{"eissn":["1558-1225"],"isbn":["9798331505691"]},"title":"Cooperative software verification via dynamic program splitting","date_created":"2025-07-16T11:32:29Z","oa_version":"None","OA_type":"closed access","publication_status":"published","conference":{"end_date":"2025-05-06","location":"Ottawa, ON, Canada","name":"ICSE: International Conference on Software Engineering","start_date":"2025-04-26"},"corr_author":"1","article_processing_charge":"No","publisher":"IEEE","acknowledgement":"This work is partially supported by the German Research Foundation (DFG) – WE2290/13-2 (Coop2), and in part by the ERC-2020-AdG 101020093.","doi":"10.1109/ICSE55347.2025.00092","author":[{"first_name":"Cedric","last_name":"Richter","full_name":"Richter, Cedric"},{"first_name":"Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","last_name":"Chalupa","full_name":"Chalupa, Marek"},{"last_name":"Jakobs","full_name":"Jakobs, Marie-Christine","first_name":"Marie-Christine"},{"full_name":"Wehrheim, Heike","last_name":"Wehrheim","first_name":"Heike"}],"project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"}],"department":[{"_id":"ToHe"}],"month":"05"},{"file_date_updated":"2025-06-02T07:10:35Z","publication":"31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems","date_updated":"2025-06-02T07:21:41Z","status":"public","page":"212-216","ec_funded":1,"scopus_import":"1","_id":"19739","language":[{"iso":"eng"}],"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."}],"type":"conference","quality_controlled":"1","has_accepted_license":"1","day":"01","citation":{"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.","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>","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>","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.","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.","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>."},"intvolume":"     15698","year":"2025","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["000"],"date_published":"2025-05-01T00:00:00Z","OA_place":"publisher","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).","oa":1,"doi":"10.1007/978-3-031-90660-2_14","volume":15698,"author":[{"id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","first_name":"Marek","last_name":"Chalupa","full_name":"Chalupa, Marek"},{"first_name":"Cedric","full_name":"Richter, Cedric","last_name":"Richter"}],"project":[{"name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","grant_number":"101020093"}],"month":"05","department":[{"_id":"ToHe"}],"tmp":{"short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"corr_author":"1","article_processing_charge":"No","publisher":"Springer Nature","publication_status":"published","conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2025-05-03","end_date":"2025-05-08","location":"Hamilton, ON, Canada"},"file":[{"checksum":"3f604f25dbe37383acb7f8308aad3ca6","file_name":"2025_TACAS_Chalupa.pdf","relation":"main_file","date_updated":"2025-06-02T07:10:35Z","file_id":"19766","creator":"dernst","access_level":"open_access","content_type":"application/pdf","success":1,"file_size":259050,"date_created":"2025-06-02T07:10:35Z"}],"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031906596"]},"title":"BUBAAK: Dynamic cooperative verification","date_created":"2025-05-25T22:17:04Z","alternative_title":["LNCS"],"oa_version":"Published Version","OA_type":"hybrid"},{"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).","doi":"10.1007/s00236-025-00509-8","oa":1,"project":[{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"},{"name":"Interface Theory for Security and Privacy","_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e","grant_number":"F8502"}],"article_type":"original","department":[{"_id":"ToHe"}],"month":"12","author":[{"full_name":"Bartocci, Ezio","last_name":"Bartocci","first_name":"Ezio"},{"first_name":"Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","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"},{"first_name":"Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87","last_name":"Nickovic","full_name":"Nickovic, Dejan"},{"last_name":"Oliveira da Costa","full_name":"Oliveira da Costa, Ana","orcid":"0000-0002-8741-5799","id":"f347ec37-6676-11ee-b395-a888cb7b4fb4","first_name":"Ana"}],"volume":62,"publisher":"Springer Nature","tmp":{"short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"corr_author":"1","article_processing_charge":"Yes (via OA deal)","related_material":{"record":[{"id":"14405","status":"public","relation":"earlier_version"}]},"publication_status":"published","file":[{"checksum":"06ed45a1218ad8464818803ae2968aaf","file_name":"2025_ActaInformatica_Bartocci.pdf","creator":"dernst","relation":"main_file","date_updated":"2026-01-05T12:26:43Z","file_id":"20944","access_level":"open_access","content_type":"application/pdf","success":1,"date_created":"2026-01-05T12:26:43Z","file_size":7117003}],"publication_identifier":{"eissn":["1432-0525"],"issn":["0001-5903"]},"arxiv":1,"oa_version":"Published Version","OA_type":"hybrid","date_created":"2025-12-29T12:07:12Z","title":"Hypernode automata","file_date_updated":"2026-01-05T12:26:43Z","publication":"Acta Informatica","date_updated":"2026-01-05T12:27:41Z","status":"public","scopus_import":"1","issue":"4","ec_funded":1,"type":"journal_article","quality_controlled":"1","language":[{"iso":"eng"}],"_id":"20866","abstract":[{"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.","lang":"eng"}],"external_id":{"arxiv":["2305.02836"]},"has_accepted_license":"1","day":"09","citation":{"ista":"Bartocci E, Chalupa M, Henzinger TA, Nickovic D, Oliveira da Costa A. 2025. Hypernode automata. Acta Informatica. 62(4), 43.","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>","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.","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>.","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>"},"year":"2025","ddc":["000"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_number":"43","intvolume":"        62","date_published":"2025-12-09T00:00:00Z","OA_place":"publisher"},{"arxiv":1,"oa_version":"Published Version","OA_type":"gold","date_created":"2026-01-29T15:39:15Z","title":"Flavors of quantifiers in hyperlogics","alternative_title":["LIPIcs"],"conference":{"start_date":"2025-12-17","name":"FSTTCS: Conference on Foundations of Software Technology and Theoretical Computer Science","location":"Pilani, India","end_date":"2025-12-19"},"publication_status":"published","file":[{"creator":"dernst","date_updated":"2026-02-11T09:33:20Z","relation":"main_file","file_id":"21213","checksum":"8188ee5c7b14193d48eeb655e9bbdc47","file_name":"2025_LIPIcS_Chalupa.pdf","success":1,"content_type":"application/pdf","file_size":933970,"date_created":"2026-02-11T09:33:20Z","access_level":"open_access"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","corr_author":"1","tmp":{"short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"article_processing_charge":"No","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.","doi":"10.4230/LIPICS.FSTTCS.2025.20","oa":1,"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","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"}],"department":[{"_id":"ToHe"}],"month":"12","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"},{"full_name":"Oliveira da Costa, Ana A","last_name":"Oliveira da Costa","id":"8b282559-50b0-11ef-861e-d6ace0d92e9b","first_name":"Ana A"}],"volume":360,"year":"2025","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["000"],"intvolume":"       360","date_published":"2025-12-09T00:00:00Z","OA_place":"publisher","type":"conference","quality_controlled":"1","_id":"21089","language":[{"iso":"eng"}],"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."}],"external_id":{"arxiv":["2510.12298"]},"has_accepted_license":"1","citation":{"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>.","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.","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.","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>","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.","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>."},"day":"09","page":"20:1-20:18","status":"public","scopus_import":"1","ec_funded":1,"file_date_updated":"2026-02-11T09:33:20Z","publication":"45th Annual Conference on Foundations of Software Technology and Theoretical Computer Science","date_updated":"2026-02-11T09:35:04Z"},{"conference":{"name":"RV: Runtime Verification","start_date":"2025-09-15","end_date":"2025-09-19","location":"Graz, Austria"},"publication_status":"published","oa_version":"Preprint","OA_type":"green","title":"Monitoring hypernode logic over infinite domains","date_created":"2026-01-29T16:04:31Z","alternative_title":["LNCS"],"arxiv":1,"publication_identifier":{"eisbn":["9783032054357"],"eissn":["1611-3349"],"issn":["0302-9743"]},"project":[{"name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"},{"name":"Interface Theory for Security and Privacy","_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e","grant_number":"F8502"}],"month":"09","department":[{"_id":"ToHe"}],"volume":16087,"author":[{"first_name":"Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","last_name":"Chalupa","full_name":"Chalupa, Marek"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Oliveira da Costa","full_name":"Oliveira da Costa, Ana A","first_name":"Ana A","id":"8b282559-50b0-11ef-861e-d6ace0d92e9b"}],"acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093 and in part by the FWF-2022-SFB F8502 (SPyCoDe).","doi":"10.1007/978-3-032-05435-7_23","oa":1,"publisher":"Springer Nature","corr_author":"1","article_processing_charge":"No","day":"13","citation":{"apa":"Chalupa, M., Henzinger, T. A., &#38; Oliveira da Costa, A. A. (2025). Monitoring hypernode logic over infinite domains. In <i>25th International Conference on Runtime Verification</i> (Vol. 16087, pp. 417–437). Graz, Austria: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-032-05435-7_23\">https://doi.org/10.1007/978-3-032-05435-7_23</a>","ieee":"M. Chalupa, T. A. Henzinger, and A. A. Oliveira da Costa, “Monitoring hypernode logic over infinite domains,” in <i>25th International Conference on Runtime Verification</i>, Graz, Austria, 2025, vol. 16087, pp. 417–437.","short":"M. Chalupa, T.A. Henzinger, A.A. Oliveira da Costa, in:, 25th International Conference on Runtime Verification, Springer Nature, 2025, pp. 417–437.","mla":"Chalupa, Marek, et al. “Monitoring Hypernode Logic over Infinite Domains.” <i>25th International Conference on Runtime Verification</i>, vol. 16087, Springer Nature, 2025, pp. 417–37, doi:<a href=\"https://doi.org/10.1007/978-3-032-05435-7_23\">10.1007/978-3-032-05435-7_23</a>.","chicago":"Chalupa, Marek, Thomas A Henzinger, and Ana A Oliveira da Costa. “Monitoring Hypernode Logic over Infinite Domains.” In <i>25th International Conference on Runtime Verification</i>, 16087:417–37. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-032-05435-7_23\">https://doi.org/10.1007/978-3-032-05435-7_23</a>.","ista":"Chalupa M, Henzinger TA, Oliveira da Costa AA. 2025. Monitoring hypernode logic over infinite domains. 25th International Conference on Runtime Verification. RV: Runtime Verification, LNCS, vol. 16087, 417–437.","ama":"Chalupa M, Henzinger TA, Oliveira da Costa AA. Monitoring hypernode logic over infinite domains. In: <i>25th International Conference on Runtime Verification</i>. Vol 16087. Springer Nature; 2025:417-437. doi:<a href=\"https://doi.org/10.1007/978-3-032-05435-7_23\">10.1007/978-3-032-05435-7_23</a>"},"type":"conference","quality_controlled":"1","_id":"21093","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"}],"language":[{"iso":"eng"}],"external_id":{"arxiv":["2508.02301"]},"main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2508.02301"}],"date_published":"2025-09-13T00:00:00Z","OA_place":"repository","year":"2025","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","intvolume":"     16087","publication":"25th International Conference on Runtime Verification","date_updated":"2026-02-16T11:59:20Z","ec_funded":1,"status":"public","page":"417-437"},{"year":"2025","ddc":["000"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","intvolume":"     15696","date_published":"2025-05-01T00:00:00Z","OA_place":"publisher","type":"conference","quality_controlled":"1","_id":"19741","abstract":[{"text":"Quantitative automata model beyond-boolean aspects of systems: every execution is mapped to a real number by incorporating weighted transitions and value functions that generalize acceptance conditions of boolean w-automata. Despite the theoretical advances in systems analysis through quantitative automata, the first comprehensive software tool for quantitative automata (Quantitative Automata Kit, or QuAK) was developed only recently. QuAK implements algorithms for solving standard decision problems, e.g., emptiness and universality, as well as constructions for safety and liveness of quantitative automata. We present the architecture of QuAK, which reflects that all of these problems reduce to either checking inclusion between two quantitative automata or computing the highest value achievable by an automaton—its so-called top value. We improve QuAK by extending these two algorithms with an option to return, alongside their results, an ultimately periodic word witnessing the algorithm’s output, as well as implementing a new safety-liveness decomposition algorithm that can handle nondeterministic automata, making QuAK more informative and capable.","lang":"eng"}],"language":[{"iso":"eng"}],"external_id":{"arxiv":["2501.16088"]},"has_accepted_license":"1","day":"01","citation":{"apa":"Chalupa, M., Henzinger, T. A., Mazzocchi, N. A., &#38; Sarac, N. E. (2025). Automating the analysis of quantitative automata with QuAK. In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 15696, pp. 303–312). Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-90643-5_16\">https://doi.org/10.1007/978-3-031-90643-5_16</a>","ieee":"M. Chalupa, T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Automating the analysis of quantitative automata with QuAK,” in <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 2025, vol. 15696, pp. 303–312.","short":"M. Chalupa, T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2025, pp. 303–312.","mla":"Chalupa, Marek, et al. “Automating the Analysis of Quantitative Automata with QuAK.” <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 15696, Springer Nature, 2025, pp. 303–12, doi:<a href=\"https://doi.org/10.1007/978-3-031-90643-5_16\">10.1007/978-3-031-90643-5_16</a>.","chicago":"Chalupa, Marek, Thomas A Henzinger, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Automating the Analysis of Quantitative Automata with QuAK.” In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 15696:303–12. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-90643-5_16\">https://doi.org/10.1007/978-3-031-90643-5_16</a>.","ista":"Chalupa M, Henzinger TA, Mazzocchi NA, Sarac NE. 2025. Automating the analysis of quantitative automata with QuAK. 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems. , LNCS, vol. 15696, 303–312.","ama":"Chalupa M, Henzinger TA, Mazzocchi NA, Sarac NE. Automating the analysis of quantitative automata with QuAK. In: <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 15696. Springer Nature; 2025:303-312. doi:<a href=\"https://doi.org/10.1007/978-3-031-90643-5_16\">10.1007/978-3-031-90643-5_16</a>"},"page":"303-312","status":"public","scopus_import":"1","ec_funded":1,"file_date_updated":"2025-06-02T08:13:11Z","date_updated":"2026-04-07T12:02:57Z","publication":"31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783031906428"]},"arxiv":1,"oa_version":"Published Version","OA_type":"hybrid","date_created":"2025-05-25T22:17:07Z","title":"Automating the analysis of quantitative automata with QuAK","alternative_title":["LNCS"],"publication_status":"published","file":[{"access_level":"open_access","content_type":"application/pdf","success":1,"date_created":"2025-06-02T08:13:11Z","file_size":420669,"checksum":"a27fa245be8d83421e9127b48a09c8af","file_name":"2025_TACAS_ChalupaMarek.pdf","file_id":"19768","creator":"dernst","relation":"main_file","date_updated":"2025-06-02T08:13:11Z"}],"publisher":"Springer Nature","tmp":{"short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"corr_author":"1","article_processing_charge":"No","related_material":{"record":[{"relation":"dissertation_contains","id":"20147","status":"public"}]},"acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093.","doi":"10.1007/978-3-031-90643-5_16","oa":1,"project":[{"name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"department":[{"_id":"ToHe"}],"month":"05","volume":15696,"author":[{"last_name":"Chalupa","full_name":"Chalupa, Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","first_name":"Marek"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Mazzocchi, Nicolas Adrien","last_name":"Mazzocchi","id":"b26baa86-3308-11ec-87b0-8990f34baa85","first_name":"Nicolas Adrien"},{"last_name":"Sarac","full_name":"Sarac, Naci E","first_name":"Naci E","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425"}]},{"citation":{"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>.","ista":"Chalupa M, Henzinger TA, Oliveira da Costa A. 2024. Monitoring extended hypernode logic. Integrated Formal Methods. , LNCS, vol. 15234, 151–171.","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>","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>","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.","short":"M. Chalupa, T.A. Henzinger, A. Oliveira da Costa, in:, Integrated Formal Methods, Springer Nature, 2024, pp. 151–171.","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>."},"day":"13","_id":"18599","abstract":[{"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.","lang":"eng"}],"language":[{"iso":"eng"}],"external_id":{"isi":["001416640500009"]},"type":"conference","quality_controlled":"1","date_published":"2024-11-13T00:00:00Z","intvolume":"     15234","year":"2024","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","publication":"Integrated Formal Methods","date_updated":"2025-09-08T14:47:22Z","isi":1,"ec_funded":1,"scopus_import":"1","status":"public","page":"151-171","publication_status":"published","title":"Monitoring extended hypernode logic","date_created":"2024-12-01T23:01:52Z","alternative_title":["LNCS"],"oa_version":"None","OA_type":"closed access","publication_identifier":{"isbn":["9783031765537"],"issn":["0302-9743"],"eissn":["1611-3349"]},"volume":15234,"author":[{"id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","first_name":"Marek","last_name":"Chalupa","full_name":"Chalupa, Marek"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000-0002-2985-7724"},{"first_name":"Ana","id":"f347ec37-6676-11ee-b395-a888cb7b4fb4","orcid":"0000-0002-8741-5799","full_name":"Oliveira da Costa, Ana","last_name":"Oliveira da Costa"}],"project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"},{"grant_number":"F8502","_id":"34a1b658-11ca-11ed-8bc3-c75229f0241e","name":"Interface Theory for Security and Privacy"}],"department":[{"_id":"ToHe"}],"month":"11","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093, and by the Austrian Science Fund (FWF) SFB project SpyCoDe F8502.","doi":"10.1007/978-3-031-76554-4_9","corr_author":"1","article_processing_charge":"No","publisher":"Springer Nature"},{"title":"Bubaak-SpLit: Split what you cannot verify (Competition contribution)","date_created":"2024-04-20T18:14:06Z","alternative_title":["LNCS"],"oa_version":"Published Version","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783031572555"],"eisbn":["9783031572562"]},"file":[{"file_name":"2024_LNCS_Chalupa.pdf","checksum":"208c855c60824bec936b8d01d0396474","file_id":"15347","creator":"cchlebak","relation":"main_file","date_updated":"2024-04-26T11:27:26Z","access_level":"open_access","date_created":"2024-04-26T11:27:26Z","file_size":577128,"content_type":"application/pdf","success":1}],"publication_status":"published","conference":{"location":"Luxembourg City, Luxembourg","end_date":"2024-04-11","start_date":"2024-04-06","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"corr_author":"1","tmp":{"short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"article_processing_charge":"Yes (in subscription journal)","publisher":"Springer Nature","volume":14572,"author":[{"first_name":"Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","full_name":"Chalupa, Marek","last_name":"Chalupa"},{"last_name":"Richter","full_name":"Richter, Cedric","first_name":"Cedric"}],"project":[{"name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"month":"04","department":[{"_id":"ToHe"}],"acknowledgement":"This work was partially supported by the ERC-2020-AdG 10102009 grant.","doi":"10.1007/978-3-031-57256-2_20","oa":1,"date_published":"2024-04-05T00:00:00Z","intvolume":"     14572","year":"2024","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","ddc":["000"],"has_accepted_license":"1","day":"05","citation":{"apa":"Chalupa, M., &#38; Richter, C. (2024). Bubaak-SpLit: Split what you cannot verify (Competition contribution). In <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 14572, pp. 353–358). Luxembourg City, Luxembourg: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-57256-2_20\">https://doi.org/10.1007/978-3-031-57256-2_20</a>","ieee":"M. Chalupa and C. Richter, “Bubaak-SpLit: Split what you cannot verify (Competition contribution),” in <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Luxembourg City, Luxembourg, 2024, vol. 14572, pp. 353–358.","short":"M. Chalupa, C. Richter, in:, 30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2024, pp. 353–358.","mla":"Chalupa, Marek, and Cedric Richter. “Bubaak-SpLit: Split What You Cannot Verify (Competition Contribution).” <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 14572, Springer Nature, 2024, pp. 353–358, doi:<a href=\"https://doi.org/10.1007/978-3-031-57256-2_20\">10.1007/978-3-031-57256-2_20</a>.","chicago":"Chalupa, Marek, and Cedric Richter. “Bubaak-SpLit: Split What You Cannot Verify (Competition Contribution).” In <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 14572:353–358. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-57256-2_20\">https://doi.org/10.1007/978-3-031-57256-2_20</a>.","ista":"Chalupa M, Richter C. 2024. Bubaak-SpLit: Split what you cannot verify (Competition contribution). 30th 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. 14572, 353–358.","ama":"Chalupa M, Richter C. Bubaak-SpLit: Split what you cannot verify (Competition contribution). In: <i>30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 14572. Springer Nature; 2024:353–358. doi:<a href=\"https://doi.org/10.1007/978-3-031-57256-2_20\">10.1007/978-3-031-57256-2_20</a>"},"_id":"15333","language":[{"iso":"eng"}],"abstract":[{"lang":"eng","text":"BUBAAK-SpLit is a tool for dynamically splitting verification tasks into parts that can then be analyzed in parallel. It is built on top of BUBAAK, a tool designed for running combinations of verifiers in parallel. In contrast to BUBAAK, that directly invokes verifiers on the inputs, BUBAAK-SpLit first starts by splitting the input program into multiple modified versions called program splits. During the splitting process, BUBAAK-SpLit utilizes a weak verifier (in our case symbolic execution with a short timelimit) to analyze each generated program split. If the weak verifier fails on a program split, we split this program split again and start the verification process again on the generated program splits. We run the splitting process until a predefined number of hard-to-verify program splits is generated or a splitting limit is reached. During the main verification phase, we run a combination of BUBAAK-LEE and SLOWBEAST in parallel on the remaining unsolved parts of the verification task."}],"external_id":{"isi":["001284187100020"]},"type":"conference","quality_controlled":"1","ec_funded":1,"scopus_import":"1","page":"353–358","status":"public","publication":"30th International Conference on Tools and Algorithms for the Construction and Analysis of Systems","date_updated":"2025-09-04T13:48:25Z","isi":1,"file_date_updated":"2024-04-26T11:27:26Z"},{"oa":1,"doi":"10.1007/978-3-031-75387-9_1","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093. N. Mazzocchi was affiliated with ISTA when his collaboration started.","volume":15222,"author":[{"full_name":"Chalupa, Marek","last_name":"Chalupa","first_name":"Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"last_name":"Mazzocchi","full_name":"Mazzocchi, Nicolas Adrien","first_name":"Nicolas Adrien","id":"b26baa86-3308-11ec-87b0-8990f34baa85"},{"full_name":"Sarac, Naci E","last_name":"Sarac","first_name":"Naci E","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425"}],"month":"10","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"}],"article_processing_charge":"Yes (in subscription journal)","corr_author":"1","tmp":{"short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"publisher":"Springer Nature","related_material":{"record":[{"relation":"dissertation_contains","id":"20147","status":"public"}]},"publication_status":"published","conference":{"start_date":"2024-10-27","name":"ISoLA: International Symposium on Leveraging Applications","location":"Crete, Greece","end_date":"2024-10-31"},"file":[{"access_level":"open_access","file_size":847422,"date_created":"2024-09-05T14:26:02Z","content_type":"application/pdf","success":1,"file_name":"isola24.pdf","checksum":"43e432f82be376434b358f3dd7a94b71","date_updated":"2024-09-05T14:26:02Z","creator":"esarac","file_id":"17635","relation":"main_file"},{"relation":"main_file","creator":"dernst","file_id":"18865","date_updated":"2025-01-21T14:39:49Z","checksum":"6bc04f07bb5612c0e7ea00ac121a69b6","file_name":"2024_LNCS_Chalupa.pdf","content_type":"application/pdf","success":1,"date_created":"2025-01-21T14:39:49Z","file_size":1358706,"access_level":"open_access"}],"arxiv":1,"publication_identifier":{"isbn":["9783031753862"],"issn":["0302-9743"],"eissn":["1611-3349"]},"title":"QuAK: Quantitative Automata Kit","alternative_title":["LNCS"],"date_created":"2024-09-05T14:27:08Z","OA_type":"hybrid","oa_version":"Published Version","file_date_updated":"2025-01-21T14:39:49Z","date_updated":"2026-04-07T12:02:57Z","publication":"12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation","isi":1,"page":"3-20","status":"public","ec_funded":1,"scopus_import":"1","external_id":{"arxiv":["2409.03569"],"isi":["001419008700001"]},"abstract":[{"text":"System behaviors are traditionally evaluated through binary classifications of correctness, which do not suffice for properties involving quantitative aspects of systems and executions. Quantitative automata offer a more nuanced approach, mapping each execution to a real number by incorporating weighted transitions and value functions generalizing acceptance conditions. In this paper, we introduce QuAK, the first tool designed to automate the analysis of quantitative automata. QuAK currently supports a variety of quantitative automaton types, including Inf, Sup, LimInf, LimSup, LimInfAvg, and LimSupAvg automata, and implements decision procedures for problems such as emptiness, universality, inclusion, equivalence, as well as for checking whether an automaton is safe, live, or constant. Additionally, QuAK is able to compute extremal values when possible, construct safety-liveness decompositions, and monitor system behaviors. We demonstrate the effectiveness of QuAK through experiments focusing on the inclusion, constant-function check, and monitoring problems.","lang":"eng"}],"_id":"17634","language":[{"iso":"eng"}],"quality_controlled":"1","type":"conference","day":"26","citation":{"ista":"Chalupa M, Henzinger TA, Mazzocchi NA, Sarac NE. 2024. QuAK: Quantitative Automata Kit. 12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation. ISoLA: International Symposium on Leveraging Applications, LNCS, vol. 15222, 3–20.","ama":"Chalupa M, Henzinger TA, Mazzocchi NA, Sarac NE. QuAK: Quantitative Automata Kit. In: <i>12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation</i>. Vol 15222. Springer Nature; 2024:3-20. doi:<a href=\"https://doi.org/10.1007/978-3-031-75387-9_1\">10.1007/978-3-031-75387-9_1</a>","chicago":"Chalupa, Marek, Thomas A Henzinger, Nicolas Adrien Mazzocchi, and Naci E Sarac. “QuAK: Quantitative Automata Kit.” In <i>12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation</i>, 15222:3–20. Springer Nature, 2024. <a href=\"https://doi.org/10.1007/978-3-031-75387-9_1\">https://doi.org/10.1007/978-3-031-75387-9_1</a>.","short":"M. Chalupa, T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, Springer Nature, 2024, pp. 3–20.","ieee":"M. Chalupa, T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “QuAK: Quantitative Automata Kit,” in <i>12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation</i>, Crete, Greece, 2024, vol. 15222, pp. 3–20.","mla":"Chalupa, Marek, et al. “QuAK: Quantitative Automata Kit.” <i>12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation</i>, vol. 15222, Springer Nature, 2024, pp. 3–20, doi:<a href=\"https://doi.org/10.1007/978-3-031-75387-9_1\">10.1007/978-3-031-75387-9_1</a>.","apa":"Chalupa, M., Henzinger, T. A., Mazzocchi, N. A., &#38; Sarac, N. E. (2024). QuAK: Quantitative Automata Kit. In <i>12th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation</i> (Vol. 15222, pp. 3–20). Crete, Greece: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-75387-9_1\">https://doi.org/10.1007/978-3-031-75387-9_1</a>"},"has_accepted_license":"1","intvolume":"     15222","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","ddc":["000"],"year":"2024","OA_place":"publisher","date_published":"2024-10-26T00:00:00Z","APC_amount":"2748 EUR"},{"language":[{"iso":"eng"}],"_id":"14076","abstract":[{"lang":"eng","text":"Hyperproperties are properties that relate multiple execution traces. Previous work on monitoring hyperproperties focused on synchronous hyperproperties, usually specified in HyperLTL. When monitoring synchronous hyperproperties, all traces are assumed to proceed at the same speed. We introduce (multi-trace) prefix transducers and show how to use them for monitoring synchronous as well as, for the first time, asynchronous hyperproperties. Prefix transducers map multiple input traces into one or more output traces by incrementally matching prefixes of the input traces against expressions similar to regular expressions. The prefixes of different traces which are consumed by a single matching step of the monitor may have different lengths. The deterministic and executable nature of prefix transducers makes them more suitable as an intermediate formalism for runtime verification than logical specifications, which tend to be highly non-deterministic, especially in the case of asynchronous hyperproperties. We report on a set of experiments about monitoring asynchronous version of observational determinism."}],"quality_controlled":"1","type":"conference","day":"01","citation":{"apa":"Chalupa, M., &#38; Henzinger, T. A. (2023). Monitoring hyperproperties with prefix transducers. In <i>23nd International Conference on Runtime Verification</i> (Vol. 14245, pp. 168–190). Thessaloniki, Greek: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-44267-4_9\">https://doi.org/10.1007/978-3-031-44267-4_9</a>","mla":"Chalupa, Marek, and Thomas A. Henzinger. “Monitoring Hyperproperties with Prefix Transducers.” <i>23nd International Conference on Runtime Verification</i>, vol. 14245, Springer Nature, 2023, pp. 168–90, doi:<a href=\"https://doi.org/10.1007/978-3-031-44267-4_9\">10.1007/978-3-031-44267-4_9</a>.","short":"M. Chalupa, T.A. Henzinger, in:, 23nd International Conference on Runtime Verification, Springer Nature, 2023, pp. 168–190.","ieee":"M. Chalupa and T. A. Henzinger, “Monitoring hyperproperties with prefix transducers,” in <i>23nd International Conference on Runtime Verification</i>, Thessaloniki, Greek, 2023, vol. 14245, pp. 168–190.","chicago":"Chalupa, Marek, and Thomas A Henzinger. “Monitoring Hyperproperties with Prefix Transducers.” In <i>23nd International Conference on Runtime Verification</i>, 14245:168–90. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-44267-4_9\">https://doi.org/10.1007/978-3-031-44267-4_9</a>.","ama":"Chalupa M, Henzinger TA. Monitoring hyperproperties with prefix transducers. In: <i>23nd International Conference on Runtime Verification</i>. Vol 14245. Springer Nature; 2023:168-190. doi:<a href=\"https://doi.org/10.1007/978-3-031-44267-4_9\">10.1007/978-3-031-44267-4_9</a>","ista":"Chalupa M, Henzinger TA. 2023. Monitoring hyperproperties with prefix transducers. 23nd International Conference on Runtime Verification. RV: Conference on Runtime Verification, LNCS, vol. 14245, 168–190."},"has_accepted_license":"1","intvolume":"     14245","ddc":["000"],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","year":"2023","date_published":"2023-10-01T00:00:00Z","file_date_updated":"2023-10-16T07:15:11Z","publication":"23nd International Conference on Runtime Verification","date_updated":"2025-04-14T09:42:55Z","status":"public","page":"168-190","ec_funded":1,"scopus_import":"1","publication_status":"published","conference":{"start_date":"2023-10-04","name":"RV: Conference on Runtime Verification","location":"Thessaloniki, Greek","end_date":"2023-10-07"},"file":[{"relation":"main_file","date_updated":"2023-10-16T07:15:11Z","creator":"dernst","file_id":"14430","file_name":"2023_LNCS_RV_Chalupa.pdf","checksum":"ee33bd6f1a26f4dae7a8192584869fd8","date_created":"2023-10-16T07:15:11Z","file_size":867256,"success":1,"content_type":"application/pdf","access_level":"open_access"}],"publication_identifier":{"eisbn":["978-3-031-44267-4"],"isbn":["978-3-031-44266-7"]},"date_created":"2023-08-16T20:46:08Z","alternative_title":["LNCS"],"title":"Monitoring hyperproperties with prefix transducers","oa_version":"Published Version","doi":"10.1007/978-3-031-44267-4_9","oa":1,"acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093. The authors would like to thank Ana Oliveira da Costa for commenting on a draft of the paper.","author":[{"id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","first_name":"Marek","last_name":"Chalupa","full_name":"Chalupa, Marek"},{"orcid":"0000-0002-2985-7724","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A","last_name":"Henzinger"}],"volume":14245,"department":[{"_id":"ToHe"}],"month":"10","project":[{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software"}],"article_processing_charge":"Yes (in subscription journal)","corr_author":"1","tmp":{"short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"publisher":"Springer Nature","related_material":{"record":[{"relation":"research_data","status":"public","id":"15035"}]}},{"type":"technical_report","_id":"12407","language":[{"iso":"eng"}],"abstract":[{"lang":"eng","text":"As the complexity and criticality of software increase every year, so does the importance of run-time monitoring. Third-party monitoring, with limited knowledge of the monitored software, and best-effort monitoring, which keeps pace with the monitored software, are especially valuable, yet underexplored areas of run-time monitoring. Most existing monitoring frameworks do not support their combination because they either require access to the monitored code for instrumentation purposes or the processing of all observed events, or both.\r\n\r\nWe present a middleware framework, VAMOS, for the run-time monitoring of software which is explicitly designed to support third-party and best-effort scenarios. The design goals of VAMOS are (i) efficiency (keeping pace at low overhead), (ii) flexibility (the ability to monitor black-box code through a variety of different event channels, and the connectability to monitors written in different specification languages), and (iii) ease-of-use. To achieve its goals, VAMOS combines aspects of event broker and event recognition systems with aspects of stream processing systems.\r\n\r\nWe implemented a prototype toolchain for VAMOS and conducted experiments including a case study of monitoring for data races. The results indicate that VAMOS enables writing useful yet efficient monitors, is compatible with a variety of event sources and monitor specifications, and simplifies key aspects of setting up a monitoring system from scratch."}],"citation":{"apa":"Chalupa, M., Mühlböck, F., Muroya Lei, S., &#38; Henzinger, T. A. (2023). <i>VAMOS: Middleware for Best-Effort Third-Party Monitoring</i>. Institute of Science and Technology Austria. <a href=\"https://doi.org/10.15479/AT:ISTA:12407\">https://doi.org/10.15479/AT:ISTA:12407</a>","mla":"Chalupa, Marek, et al. <i>VAMOS: Middleware for Best-Effort Third-Party Monitoring</i>. Institute of Science and Technology Austria, 2023, doi:<a href=\"https://doi.org/10.15479/AT:ISTA:12407\">10.15479/AT:ISTA:12407</a>.","ieee":"M. Chalupa, F. Mühlböck, S. Muroya Lei, and T. A. Henzinger, <i>VAMOS: Middleware for Best-Effort Third-Party Monitoring</i>. Institute of Science and Technology Austria, 2023.","short":"M. Chalupa, F. Mühlböck, S. Muroya Lei, T.A. Henzinger, VAMOS: Middleware for Best-Effort Third-Party Monitoring, Institute of Science and Technology Austria, 2023.","chicago":"Chalupa, Marek, Fabian Mühlböck, Stefanie Muroya Lei, and Thomas A Henzinger. <i>VAMOS: Middleware for Best-Effort Third-Party Monitoring</i>. Institute of Science and Technology Austria, 2023. <a href=\"https://doi.org/10.15479/AT:ISTA:12407\">https://doi.org/10.15479/AT:ISTA:12407</a>.","ama":"Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. <i>VAMOS: Middleware for Best-Effort Third-Party Monitoring</i>. Institute of Science and Technology Austria; 2023. doi:<a href=\"https://doi.org/10.15479/AT:ISTA:12407\">10.15479/AT:ISTA:12407</a>","ista":"Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. 2023. VAMOS: Middleware for Best-Effort Third-Party Monitoring, Institute of Science and Technology Austria, 38p."},"day":"27","has_accepted_license":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["005"],"year":"2023","date_published":"2023-01-27T00:00:00Z","file_date_updated":"2023-01-27T03:18:34Z","date_updated":"2025-09-09T12:25:29Z","status":"public","page":"38","ec_funded":1,"publication_status":"published","file":[{"content_type":"application/pdf","success":1,"file_size":662409,"date_created":"2023-01-27T03:18:34Z","access_level":"open_access","file_id":"12408","date_updated":"2023-01-27T03:18:34Z","creator":"fmuehlbo","relation":"main_file","checksum":"55426e463fdeafe9777fc3ff635154c7","file_name":"main.pdf"}],"keyword":["runtime monitoring","best effort","third party"],"publication_identifier":{"eissn":["2664-1690"]},"oa_version":"Published Version","title":"VAMOS: Middleware for Best-Effort Third-Party Monitoring","alternative_title":["IST Austria Technical Report"],"date_created":"2023-01-27T03:18:08Z","doi":"10.15479/AT:ISTA:12407","oa":1,"acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093. \r\nThe authors would like to thank the anonymous FASE reviewers for their valuable feedback and suggestions.","month":"01","department":[{"_id":"ToHe"}],"project":[{"grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software"}],"author":[{"id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","first_name":"Marek","last_name":"Chalupa","full_name":"Chalupa, Marek"},{"full_name":"Mühlböck, Fabian","last_name":"Mühlböck","orcid":"0000-0003-1548-0177","first_name":"Fabian","id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425"},{"id":"a376de31-8972-11ed-ae7b-d0251c13c8ff","first_name":"Stefanie","last_name":"Muroya Lei","full_name":"Muroya Lei, Stefanie"},{"orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A"}],"publisher":"Institute of Science and Technology Austria","article_processing_charge":"No","tmp":{"short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"corr_author":"1","related_material":{"record":[{"id":"12856","status":"public","relation":"later_version"}]}},{"file_date_updated":"2023-04-25T06:58:36Z","isi":1,"date_updated":"2025-09-09T12:24:56Z","publication":"Tools and Algorithms for the Construction and Analysis of Systems","page":"535-540","status":"public","scopus_import":"1","ec_funded":1,"quality_controlled":"1","type":"conference","external_id":{"isi":["001288698100041"]},"abstract":[{"lang":"eng","text":"The main idea behind BUBAAK is to run multiple program analyses in parallel and use runtime monitoring and enforcement to observe and control their progress in real time. The analyses send information about (un)explored states of the program and discovered invariants to a monitor. The monitor processes the received data and can force an analysis to stop the search of certain program parts (which have already been analyzed by other analyses), or to make it utilize a program invariant found by another analysis.\r\nAt SV-COMP  2023, the implementation of data exchange between the monitor and the analyses was not yet completed, which is why BUBAAK only ran several analyses in parallel, without any coordination. Still, BUBAAK won the meta-category FalsificationOverall and placed very well in several other (sub)-categories of the competition."}],"_id":"12854","language":[{"iso":"eng"}],"citation":{"ama":"Chalupa M, Henzinger TA. Bubaak: Runtime monitoring of program verifiers. In: <i>Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 13994. Springer Nature; 2023:535-540. doi:<a href=\"https://doi.org/10.1007/978-3-031-30820-8_32\">10.1007/978-3-031-30820-8_32</a>","ista":"Chalupa M, Henzinger TA. 2023. Bubaak: Runtime monitoring of program verifiers. Tools and Algorithms for the Construction and Analysis of Systems. TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 13994, 535–540.","chicago":"Chalupa, Marek, and Thomas A Henzinger. “Bubaak: Runtime Monitoring of Program Verifiers.” In <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, 13994:535–40. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-30820-8_32\">https://doi.org/10.1007/978-3-031-30820-8_32</a>.","mla":"Chalupa, Marek, and Thomas A. Henzinger. “Bubaak: Runtime Monitoring of Program Verifiers.” <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 13994, Springer Nature, 2023, pp. 535–40, doi:<a href=\"https://doi.org/10.1007/978-3-031-30820-8_32\">10.1007/978-3-031-30820-8_32</a>.","ieee":"M. Chalupa and T. A. Henzinger, “Bubaak: Runtime monitoring of program verifiers,” in <i>Tools and Algorithms for the Construction and Analysis of Systems</i>, Paris, France, 2023, vol. 13994, pp. 535–540.","short":"M. Chalupa, T.A. Henzinger, in:, Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2023, pp. 535–540.","apa":"Chalupa, M., &#38; Henzinger, T. A. (2023). Bubaak: Runtime monitoring of program verifiers. In <i>Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 13994, pp. 535–540). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-30820-8_32\">https://doi.org/10.1007/978-3-031-30820-8_32</a>"},"day":"20","has_accepted_license":"1","ddc":["000"],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","year":"2023","intvolume":"     13994","date_published":"2023-04-20T00:00:00Z","doi":"10.1007/978-3-031-30820-8_32","oa":1,"acknowledgement":"This work was supported by the ERC-2020-AdG 10102009 grant.","department":[{"_id":"ToHe"}],"month":"04","project":[{"grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software"}],"author":[{"id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","first_name":"Marek","full_name":"Chalupa, Marek","last_name":"Chalupa"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724"}],"volume":13994,"publisher":"Springer Nature","article_processing_charge":"No","tmp":{"short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"corr_author":"1","conference":{"end_date":"2023-04-27","location":"Paris, France","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2023-04-22"},"publication_status":"published","file":[{"creator":"dernst","date_updated":"2023-04-25T06:58:36Z","file_id":"12864","relation":"main_file","file_name":"2023_LNCS_Chalupa.pdf","checksum":"120d2c2a38384058ad0630fdf8288312","file_size":16096413,"date_created":"2023-04-25T06:58:36Z","content_type":"application/pdf","success":1,"access_level":"open_access"}],"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031308192"],"eisbn":["9783031308208"]},"oa_version":"Published Version","title":"Bubaak: Runtime monitoring of program verifiers","date_created":"2023-04-20T08:22:53Z","alternative_title":["LNCS"]},{"department":[{"_id":"ToHe"}],"month":"04","project":[{"name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d"}],"author":[{"full_name":"Chalupa, Marek","last_name":"Chalupa","first_name":"Marek","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463"},{"full_name":"Mühlböck, Fabian","last_name":"Mühlböck","id":"6395C5F6-89DF-11E9-9C97-6BDFE5697425","first_name":"Fabian","orcid":"0000-0003-1548-0177"},{"full_name":"Muroya Lei, Stefanie","last_name":"Muroya Lei","first_name":"Stefanie","id":"a376de31-8972-11ed-ae7b-d0251c13c8ff"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724"}],"volume":13991,"oa":1,"doi":"10.1007/978-3-031-30826-0_15","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093. The authors would like to thank the anonymous FASE reviewers for their valuable feedback and suggestions.","related_material":{"record":[{"id":"18169","status":"public","relation":"later_version"},{"relation":"earlier_version","id":"12407","status":"public"}]},"publisher":"Springer Nature","article_processing_charge":"No","tmp":{"short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"corr_author":"1","file":[{"success":1,"content_type":"application/pdf","file_size":580828,"date_created":"2023-04-25T07:16:36Z","access_level":"open_access","relation":"main_file","creator":"dernst","date_updated":"2023-04-25T07:16:36Z","file_id":"12865","checksum":"17a7c8e08be609cf2408d37ea55e322c","file_name":"2023_LNCS_ChalupaM.pdf"}],"conference":{"name":"FASE: Fundamental Approaches to Software Engineering","start_date":"2023-04-22","end_date":"2023-04-27","location":"Paris, France"},"publication_status":"published","oa_version":"Published Version","alternative_title":["LNCS"],"date_created":"2023-04-20T08:29:42Z","title":"Vamos: Middleware for best-effort third-party monitoring","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"eisbn":["9783031308260"],"isbn":["9783031308253"]},"isi":1,"publication":"Fundamental Approaches to Software Engineering","date_updated":"2025-09-09T12:25:29Z","file_date_updated":"2023-04-25T07:16:36Z","scopus_import":"1","ec_funded":1,"page":"260-281","status":"public","day":"20","citation":{"mla":"Chalupa, Marek, et al. “Vamos: Middleware for Best-Effort Third-Party Monitoring.” <i>Fundamental Approaches to Software Engineering</i>, vol. 13991, Springer Nature, 2023, pp. 260–81, doi:<a href=\"https://doi.org/10.1007/978-3-031-30826-0_15\">10.1007/978-3-031-30826-0_15</a>.","ieee":"M. Chalupa, F. Mühlböck, S. Muroya Lei, and T. A. Henzinger, “Vamos: Middleware for best-effort third-party monitoring,” in <i>Fundamental Approaches to Software Engineering</i>, Paris, France, 2023, vol. 13991, pp. 260–281.","short":"M. Chalupa, F. Mühlböck, S. Muroya Lei, T.A. Henzinger, in:, Fundamental Approaches to Software Engineering, Springer Nature, 2023, pp. 260–281.","apa":"Chalupa, M., Mühlböck, F., Muroya Lei, S., &#38; Henzinger, T. A. (2023). Vamos: Middleware for best-effort third-party monitoring. In <i>Fundamental Approaches to Software Engineering</i> (Vol. 13991, pp. 260–281). Paris, France: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-30826-0_15\">https://doi.org/10.1007/978-3-031-30826-0_15</a>","ama":"Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. Vamos: Middleware for best-effort third-party monitoring. In: <i>Fundamental Approaches to Software Engineering</i>. Vol 13991. Springer Nature; 2023:260-281. doi:<a href=\"https://doi.org/10.1007/978-3-031-30826-0_15\">10.1007/978-3-031-30826-0_15</a>","ista":"Chalupa M, Mühlböck F, Muroya Lei S, Henzinger TA. 2023. Vamos: Middleware for best-effort third-party monitoring. Fundamental Approaches to Software Engineering. FASE: Fundamental Approaches to Software Engineering, LNCS, vol. 13991, 260–281.","chicago":"Chalupa, Marek, Fabian Mühlböck, Stefanie Muroya Lei, and Thomas A Henzinger. “Vamos: Middleware for Best-Effort Third-Party Monitoring.” In <i>Fundamental Approaches to Software Engineering</i>, 13991:260–81. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/978-3-031-30826-0_15\">https://doi.org/10.1007/978-3-031-30826-0_15</a>."},"has_accepted_license":"1","quality_controlled":"1","type":"conference","external_id":{"isi":["001284136600015"]},"_id":"12856","abstract":[{"text":"As the complexity and criticality of software increase every year, so does the importance of run-time monitoring. Third-party monitoring, with limited knowledge of the monitored software, and best-effort monitoring, which keeps pace with the monitored software, are especially valuable, yet underexplored areas of run-time monitoring. Most existing monitoring frameworks do not support their combination because they either require access to the monitored code for instrumentation purposes or the processing of all observed events, or both.\r\n\r\nWe present a middleware framework, VAMOS, for the run-time monitoring of software which is explicitly designed to support third-party and best-effort scenarios. The design goals of VAMOS are (i) efficiency (keeping pace at low overhead), (ii) flexibility (the ability to monitor black-box code through a variety of different event channels, and the connectability to monitors written in different specification languages), and (iii) ease-of-use. To achieve its goals, VAMOS combines aspects of event broker and event recognition systems with aspects of stream processing systems.\r\nWe implemented a prototype toolchain for VAMOS and conducted experiments including a case study of monitoring for data races. The results indicate that VAMOS enables writing useful yet efficient monitors, is compatible with a variety of event sources and monitor specifications, and simplifies key aspects of setting up a monitoring system from scratch.","lang":"eng"}],"language":[{"iso":"eng"}],"date_published":"2023-04-20T00:00:00Z","ddc":["000"],"user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","year":"2023","intvolume":"     13991"},{"date_updated":"2025-04-14T09:42:55Z","author":[{"full_name":"Chalupa, Marek","last_name":"Chalupa","id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","first_name":"Marek"},{"last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","orcid":"0000-0002-2985-7724"}],"project":[{"name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}],"department":[{"_id":"ToHe"}],"month":"07","oa":1,"doi":"10.5281/ZENODO.8191723","ec_funded":1,"related_material":{"record":[{"status":"public","id":"14076","relation":"used_in_publication"}]},"corr_author":"1","tmp":{"short":"CC BY (4.0)","image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"article_processing_charge":"No","publisher":"Zenodo","status":"public","has_accepted_license":"1","citation":{"ama":"Chalupa M, Henzinger TA. Monitoring hyperproperties with prefix transducers. 2023. doi:<a href=\"https://doi.org/10.5281/ZENODO.8191723\">10.5281/ZENODO.8191723</a>","ista":"Chalupa M, Henzinger TA. 2023. Monitoring hyperproperties with prefix transducers, Zenodo, <a href=\"https://doi.org/10.5281/ZENODO.8191723\">10.5281/ZENODO.8191723</a>.","chicago":"Chalupa, Marek, and Thomas A Henzinger. “Monitoring Hyperproperties with Prefix Transducers.” Zenodo, 2023. <a href=\"https://doi.org/10.5281/ZENODO.8191723\">https://doi.org/10.5281/ZENODO.8191723</a>.","mla":"Chalupa, Marek, and Thomas A. Henzinger. <i>Monitoring Hyperproperties with Prefix Transducers</i>. Zenodo, 2023, doi:<a href=\"https://doi.org/10.5281/ZENODO.8191723\">10.5281/ZENODO.8191723</a>.","ieee":"M. Chalupa and T. A. Henzinger, “Monitoring hyperproperties with prefix transducers.” Zenodo, 2023.","short":"M. Chalupa, T.A. Henzinger, (2023).","apa":"Chalupa, M., &#38; Henzinger, T. A. (2023). Monitoring hyperproperties with prefix transducers. Zenodo. <a href=\"https://doi.org/10.5281/ZENODO.8191723\">https://doi.org/10.5281/ZENODO.8191723</a>"},"day":"28","_id":"15035","abstract":[{"text":"This artifact aims to reproduce experiments from the paper Monitoring Hyperproperties With Prefix Transducers accepted at RV'23, and give further pointers to implementation of prefix transducers.\r\nIt has two parts: a pre-compiled docker image and sources that one can use to compile (locally or in docker) the software and run the experiments.","lang":"eng"}],"type":"research_data_reference","date_published":"2023-07-28T00:00:00Z","title":"Monitoring hyperproperties with prefix transducers","date_created":"2024-02-28T07:34:34Z","oa_version":"Published Version","main_file_link":[{"url":"https://doi.org/10.5281/zenodo.8191722","open_access":"1"}],"year":"2023","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","ddc":["000"]}]