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.

Research

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.

News

Sep ‘24. Our paper QuAK: Quantitative Automata Kit will appear in ISoLA 2024 as an invited paper.

Sep ‘24. I am attending AVM 2024 to present our work on the safety and liveness of quantitative properties and automata. Come say hi!

Jun ‘24. Our paper Approximate Distributed Monitoring under Partial Synchrony: Balancing Speed and Accuracy is accepted for publication at RV 2024.

Jun ‘24. I am visiting the DEVINE team to talk about our work on the safety and liveness of quantitative properties and automata. Many thanks to Ocan Sankur for the invitation!

Jun ‘24. Our paper Strategic Dominance: A New Preorder for Nondeterministic Processes is accepted for publication at CONCUR 2024.