Home

I am the PI of the MSCA PF project CORPORA hosted by the TrustCPS group led by Univ-Prof Ezio Bartocci at TU Wien.

My research interests cover formal methods for the verification of safety-critical and real-time systems, focusing on temporal logic, formal languages and automata theory.

I am currently working on context-free temporal logic and (probabilistic) pushdown model checking. In particular, I introduced a new temporal logic (POTL) based on Operator Precedence Languages, with the purpose of allowing better and more general modelling and specification of recursive programs. Within CORPORA, I am studying ways of verifying recursive probabilistic programs through probabilistic pushdown model checking.

I am also interested in the verification of floating-point computations, as well as approximate computing. I collaborated in the development of TAFFO, a compiler-based precision-tuning framework.

Previously, I was a Ph.D. candidate and then a PostDoc in the deepse group, at DEIB, Politecnico di Milano, where I was involved in the PIACERE H2020 project, in which I was investigating ways of model checking Infrastructure-as-Code.

News

• 2025/06/11: our paper “A Tree-Shaped Tableau for Checking the Satisfiability of Signal Temporal Logic with Bounded Temporal Operators” has been accepted at EMSOFT 2025!
• 2025/05/22: our paper “Decentralized Planning Using Probabilistic Hyperproperties” has been awarded the Best Student Paper Award at AAMAS 2025!
• 2025/05/20: our paper “POPACheck: A Model Checker for Probabilistic Pushdown Automata” has been accepted at CAV 2025!
• 2024/12/20: I’ll be co-chairing the VeriProp 2025 Workshop @ CAV 2025
• 2024/08/13: I’ll serve on the OOPSLA 2024-25 Review Committee

Contact

The best way to contact me is by email: michele.chiari@tuwien.ac.at
GitHub: michiari LinkedIn: Michele Chiari

Quite often, you may also find me here:
TrustCPS Group – TU Wien
Office 27, Floor 3, Building DE
Treitlstraße 3, 1040, Vienna, Austria
+43 1 58801 740033