@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{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},
}

@unpublished{9281,
  abstract     = {We comment on two formal proofs of Fermat's sum of two squares theorem, written using the Mathematical Components libraries of the Coq proof assistant. The first one follows Zagier's celebrated one-sentence proof; the second follows David Christopher's recent new proof relying on partition-theoretic arguments. Both formal proofs rely on a general property of involutions of finite sets, of independent interest. The proof technique consists for the most part of automating recurrent tasks (such as case distinctions and computations on natural numbers) via ad hoc tactics.},
  author       = {Dubach, Guillaume and Mühlböck, Fabian},
  booktitle    = {arXiv},
  title        = {{Formal verification of Zagier's one-sentence proof}},
  doi          = {10.48550/arXiv.2103.11389},
  year         = {2021},
}

@inproceedings{10108,
  abstract     = {We argue that the time is ripe to investigate differential monitoring, in which the specification of a program's behavior is implicitly given by a second program implementing the same informal specification. Similar ideas have been proposed before, and are currently implemented in restricted form for testing and specialized run-time analyses, aspects of which we combine. We discuss the challenges of implementing differential monitoring as a general-purpose, black-box run-time monitoring framework, and present promising results of a preliminary implementation, showing low monitoring overheads for diverse programs.},
  author       = {Mühlböck, Fabian and Henzinger, Thomas A},
  booktitle    = {International Conference on Runtime Verification},
  isbn         = {978-3-030-88493-2},
  issn         = {1611-3349},
  keywords     = {run-time verification, software engineering, implicit specification},
  location     = {Virtual},
  pages        = {231--243},
  publisher    = {Springer Nature},
  title        = {{Differential monitoring}},
  doi          = {10.1007/978-3-030-88494-9_12},
  volume       = {12974},
  year         = {2021},
}

@article{10153,
  abstract     = {Gradual typing is a principled means for mixing typed and untyped code. But typed and untyped code often exhibit different programming patterns. There is already substantial research investigating gradually giving types to code exhibiting typical untyped patterns, and some research investigating gradually removing types from code exhibiting typical typed patterns. This paper investigates how to extend these established gradual-typing concepts to give formal guarantees not only about how to change types as code evolves but also about how to change such programming patterns as well.

In particular, we explore mixing untyped "structural" code with typed "nominal" code in an object-oriented language. But whereas previous work only allowed "nominal" objects to be treated as "structural" objects, we also allow "structural" objects to dynamically acquire certain nominal types, namely interfaces. We present a calculus that supports such "cross-paradigm" code migration and interoperation in a manner satisfying both the static and dynamic gradual guarantees, and demonstrate that the calculus can be implemented efficiently.},
  author       = {Mühlböck, Fabian and Tate, Ross},
  issn         = {2475-1421},
  journal      = {Proceedings of the ACM on Programming Languages},
  keywords     = {gradual typing, gradual guarantee, nominal, structural, call tags},
  location     = {Chicago, IL, United States},
  publisher    = {Association for Computing Machinery},
  title        = {{Transitioning from structural to nominal code with efficient gradual typing}},
  doi          = {10.1145/3485504},
  volume       = {5},
  year         = {2021},
}

@misc{9946,
  abstract     = {We argue that the time is ripe to investigate differential monitoring, in which the specification of a program's behavior is implicitly given by a second program implementing the same informal specification. Similar ideas have been proposed before, and are currently implemented in restricted form for testing and specialized run-time analyses, aspects of which we combine. We discuss the challenges of implementing differential monitoring as a general-purpose, black-box run-time monitoring framework, and present promising results of a preliminary implementation, showing low monitoring overheads for diverse programs.},
  author       = {Mühlböck, Fabian and Henzinger, Thomas A},
  issn         = {2664-1690},
  keywords     = {run-time verification, software engineering, implicit specification},
  pages        = {17},
  publisher    = {IST Austria},
  title        = {{Differential monitoring}},
  doi          = {10.15479/AT:ISTA:9946},
  year         = {2021},
}