I am a Ph.D. student in the Trustworthy Cyber-Physical Systems Research Group at TU Wien, under the supervision of Prof. Ezio Bartocci, Dr. Michele Chiari and Prof. Laura Kovács. I am also part of the LogiCS@TUWien Doctoral Programme.

I work on verification and synthesis problems for probabilistic programs and systems, both theoretically and practically. The main hammer I use is probabilistic model checking. My interests cover automata theory, formal languages, formal methods, temporal logics, probabilistic programming and Bayesian inference, and planning techniques in probabilistic environments.

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.

I am passionate about functional programming and in particular the Haskell programming language.

Besides computer science research, I love studying history.

News

• [May 2025] I attended AAMAS'25, where I presented our paper Decentralized Planning Using Probabilistic Hyperproperties. It has been awarded the Best Student Paper Award! Congratulations and many thanks to all coauthors.
• [May 2025] Our paper POPACheck: A Model Checker for Probabilistic Pushdown Automata has been accepted as a tool paper at CAV'25. A preprint is available here.
• [Apr. 2025] I gave a talk entitled Exact Inference for Nested Discrete Probabilistic Programs at the OXCAV seminar.
• [Apr. 2025] I visited Prof. Stefan Kiefer at the University of Oxford.
• [Feb. 2025] A preprint of our paper Decentralized Planning Using Probabilistic Hyperproperties is available here.
• [Jan. 2025] I presented an extended abstract titled Exact Inference for Nested Discrete Probabilistic Programs at the LAnguages For Inference Workshop (LAFI), colocated with POPL'25.
• Show more
[Dec. 2024] Our paper Decentralized Planning Using Probabilistic Hyperproperties has been accepted as a full paper at AAMAS'25. A preprint version is coming soon.
[Nov. 2024] I visited Prof. Milan Češka at Brno University of Technology, where I gave a talk entitled Model Checking Recursive Probabilistic Programs.
[Oct. 2024] I attended the amazing Probability In Computer Science (PICS) Ph.D. school in Copenhagen.
[Sept. 2024] I attended Reachability Problems (RP).
[July 2024] I gave a talk entitled Deductive Controller Synthesis for Probabilistic Hyperproperties at AHyper in Vienna.
[Nov. 2023 - Jan. 2024] I visited the MOVES group at RWTH Aachen headed by Prof. Joost-Pieter Katoen.
[Sept. 2023] I gave a presentation at Quantitative Evaluations of SysTems (QEST).

Peer-Reviewed Publications

Other Works

Tools

POMC

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 domain-specific programming language, MiniProc, and specifications expressed in the logic POTL (standing for Precedence Oriented Temporal Logic). The tool is written in Haskell.

POPACheck

An extension of POMC towards the verification of probabilistic recursive programs. It support a custom domain-specific programming language, MiniProb, and specifications in LTL and a fragment of POTL. The extension is written in Haskell as well.

HyperPAYNT / PHSynt

Two tools for synthesizing controllers for Markov Decision Processes against probabilistic hyperproperty specifications. They are extensions of PAYNT, and use a customized version of STORM as underlying model checker. The tools are written in Python.

Teaching

I am tutor for the course Advanced Functional Programming [SS22][SS23][SS24][SS25], professor Jens Knoop. In particular, I maintain the final project, MiniCheck.

Service

Artifact Evaluation Committee

• [CAV 24] [FM 24]

Subreviewer

• [OOPSLA'25] [SAC-SVT'25] [FM'23] [TACAS'23] [QEST'23] [QEST'22]

Contact

Address: Treitlstrasse 3, 1040 Wien (AT)
Office: Third Floor, Office DE 03 20.
Email: name.surname(at)tuwien.ac.at