I am a Ph.D. student in the Trustworthy Cyber-Physical Systems Research Group at TU Wien, under the supervision of Ezio Bartocci, Michele Chiari and Laura Kovács. I am also part of the LogiCS doctoral programme.
I am interested in verification and synthesis problems for probabilistic programs and systems. The main hammer I use is model checking and logical formalisms. Within Corpora Lab we investigate programs that involve both recursion and randomization, while in ProbIng Lab we analyse so called probabilistic hyperproperties, i.e. properties correlating multiple executions of a probabilistic system.
Besides computer science research, I love studying history.
The Precedence Oriented Model Checker is a model checker for recursive procedural programs and context-free properties such as pre/post conditions and exception safety. It supports a custom programming language, MiniProc, and specifications expressed in the logic POTL (standing for Precedence Oriented Temporal Logic). An extension for probabilistic recursive programs is ongoing work. The tool is written in Haskell.
A tool for synthesizing controllers for Markov Decision Processes against probabilistic hyperproperty specifications. It is an extension of PAYNT, and uses STORM as underlying model checker. The tool is written in Python.
I am tutor for the course Advanced Functional Programming [SS22][SS23][SS24], professor Jens Knoop. In particular, I maintain the final project, MiniCheck.
Address: Treitlstrasse 3, 1040 Wien (AT)
Office Location: Third Floor, Office DE 03 20.
Email: name.surname(at)tuwien.ac.at
[ORCID]