@inproceedings{12854, abstract = {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. At 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.}, author = {Chalupa, Marek and Henzinger, Thomas A}, booktitle = {Tools and Algorithms for the Construction and Analysis of Systems}, isbn = {9783031308192}, issn = {1611-3349}, location = {Paris, France}, pages = {535--540}, publisher = {Springer Nature}, title = {{Bubaak: Runtime monitoring of program verifiers}}, doi = {10.1007/978-3-031-30820-8_32}, volume = {13994}, year = {2023}, } @inproceedings{12856, abstract = {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. We 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. We 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.}, author = {Chalupa, Marek and Mühlböck, Fabian and Muroya Lei, Stefanie and Henzinger, Thomas A}, booktitle = {Fundamental Approaches to Software Engineering}, isbn = {9783031308253}, issn = {1611-3349}, location = {Paris, France}, pages = {260--281}, publisher = {Springer Nature}, title = {{Vamos: Middleware for best-effort third-party monitoring}}, doi = {10.1007/978-3-031-30826-0_15}, volume = {13991}, year = {2023}, } @misc{12407, abstract = {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. We 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. We 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.}, author = {Chalupa, Marek and Mühlböck, Fabian and Muroya Lei, Stefanie and Henzinger, Thomas A}, issn = {2664-1690}, keywords = {runtime monitoring, best effort, third party}, pages = {38}, publisher = {Institute of Science and Technology Austria}, title = {{VAMOS: Middleware for Best-Effort Third-Party Monitoring}}, doi = {10.15479/AT:ISTA:12407}, year = {2023}, } @inproceedings{14076, abstract = {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.}, author = {Chalupa, Marek and Henzinger, Thomas A}, booktitle = {23nd International Conference on Runtime Verification}, isbn = {978-3-031-44266-7}, location = {Thessaloniki, Greek}, pages = {168--190}, publisher = {Springer Nature}, title = {{Monitoring hyperproperties with prefix transducers}}, doi = {10.1007/978-3-031-44267-4_9}, volume = {14245}, year = {2023}, } @misc{15035, abstract = {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. It 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.}, author = {Chalupa, Marek and Henzinger, Thomas A}, publisher = {Zenodo}, title = {{Monitoring hyperproperties with prefix transducers}}, doi = {10.5281/ZENODO.8191723}, year = {2023}, }