We enable our tool Quantitative Automata Kit (QuAK) to automatically analyze performance measures whose values can grow arbitrarily large, such as response times.
About
I am a Marie Skłodowska-Curie Postdoctoral Fellow at the CISPA Helmholtz Center for Information Security and a visiting researcher at the Technical University of Munich (TUM), working in the Reactive Systems Group led by Bernd Finkbeiner. Before that, I completed my PhD in 2025 at the Institute of Science and Technology Austria (ISTA) under Tom Henzinger's supervision.
My research aims to help people build dependable computer systems. To this end, I develop theories and algorithms for formally specifying requirements and verifying systems against them.
A central challenge motivating my work is to ensure that these systems align with human values such as privacy, fairness, and explainability. I work toward a unified framework for efficiently measuring how well systems satisfy such requirements. My MSCA Postdoctoral Fellowship project QHyperSTAR lays the foundations for this approach by advancing the theory of quantitative hyperproperties and developing memory-efficient runtime monitoring algorithms.
Selected publications
We introduce the first dedicated specification language for quantitative hyperproperties, which assign values to sets or probability distributions of infinite executions.
We generalize the safety-liveness classification to quantitative properties and give decision procedures and decomposition algorithms for quantitative automata.
We develop a theory of quantitative runtime monitoring that formalizes how monitors estimate property values from finite observations.
We accelerate the monitoring of distributed systems with bounded clock skew using sound approximations that achieve speedups of up to five orders of magnitude.
News
- Jun '26
- Our paper Monitoring Discounted Sum Properties is accepted for publication at CONCUR 2026.
- Apr '26
- Our paper Extending QuAK with Nested Quantitative Automata is accepted for publication at CAV 2026.
- Feb '26
- My MSCA Postdoctoral Fellowship project Quantitative Hyperproperties: Specification, Taxonomy, and Runtime Monitoring (QHyperSTAR) has been selected for funding!
- Feb '26
- Our paper Quantitative Monitoring of Signal First-Order Logic is accepted for publication at FM 2026.
- Oct '25
- I joined the Reactive Systems Group at CISPA Helmholtz Center for Information Security as a postdoctoral researcher.