I am a PhD candidate in computer science at the Institute of Science and Technology Austria (ISTA), where I am supervised by Tom Henzinger.
My research aims to establish a framework for online and best-effort monitoring for quantitative specifications, highlighting various tradeoffs in monitor design. I am also interested in runtime verification and formal methods in general, with a soft spot for automata theory.
Runtime verification (RV) is a lightweight, dynamic technique that determines whether a system’s run satisfies its specification. For this, a monitor watches a trace of a system and, if possible, decides after observing each finite prefix whether or not the unknown infinite trace meets a given specification. Theoretically, RV moves the burden from emptiness checking in static verification to membership checking, an easier problem. This shift introduces the opportunity to use more powerful formalisms.
My research focuses on abstractions that enable reasoning about quantitative information and moving RV to a quantitative setting. Such a setting is attractive because quantitative verdicts can be approximate and thus compared regarding their precision, which may be traded against monitor resources. I aim to develop a framework for online and best-effort quantitative monitoring that subsumes a cost-centric theory of monitorability and a precision-cost theory of approximate monitoring. Moreover, I plan to extend the framework to monitors that take corrective action and decentralized monitoring.
Read my PhD research proposal here.
Jun ‘23. Our paper Safety and Liveness of Quantitative Automata is accepted for publication at CONCUR 2023.
Apr ‘23. Our paper Regular Methods for Operator Precedence Languages is accepted for publication at ICALP 2023.
Mar ‘23. I will be attending ETAPS 2023 to present our work at FoSSaCS. Come say hi!
Dec ‘22. Our paper Quantitative Safety and Liveness is accepted for publication at FoSSaCS 2023.