Hazem Torfah

About me

I was a Ph.D. student in the Reactive Systems Group at Saarland University. I defended my thesis with the title Model Counting for Reactive Systems on Dec. 5th 2019. I am currently a postdoctoral researcher in the group of professor Sanjit A. Seshia at UC Berkeley, California.


Reactive Systems Group
Universität des Saarlandes
Campus E1.1 R. 1.15
D-66123, Saarbrücken

Phone: +49 681 302 5663
eMail: lastname at react.uni-saarland.de

Research Interests

My research interests are the specification, verification, monitoring and synthesis of reactive systems. I lay the focus on developing quantitative variants of verification and synthesis and algorithms for solving these problems.


I am a member of the program committee for RV 2020.


[DFT19b] Approximate Automata for Omega-regular Languages.
With Rayna Dimitrova and Bernd Finkbeiner
@ATVA 2019.
[T19] Stream-based Monitors for Real-time Properties. @RV 2019 (Invited Paper).
[BFST19] FPGA Stream-Monitoring of Real-time Properties.
With Jan Baumeister, Bernd Finkbeiner and Maximilian Schwenger
@EMSOFT 2019.
[DFT19] Synthesizing Approximate Implementations for Unrealizable Specifications.
With Rayna Dimitrova and Bernd Finkbeiner
@CAV 2019.
[FFS+19b] StreamLAB: Stream-based Monitoring of Cyber-physical Systems.
With Peter Faymonville, Bernd Finkbeiner, Malte Schledjewski, Maximilian Schwenger, Marvin Stenger and Leander Tentrup
@CAV 2019.
[FHT19] Canonical Representations of k-Safety Hyperproperties.
With Bernd Finkbeiner and Lennart Haas
@CSF 2019.
[FHT18] Model Checking Quantitative Hyperproperties.
With Bernd Finkbeiner and Christopher Hahn
@CAV 2018.
[KGT18] The Challenges in Specifying and Explaining Synthesized Implementations of Reactive Systems.
With Hadas Kress-Gazit
@CREST 2018.
[FT17] The Density of Linear-time Properties.
With Bernd Finkbeiner
@ATVA 2017.
[TZ16] The Complexity of Counting Models of Linear-time Temporal Logic.
With Martin Zimmermann
@Acta Informatica. This is a journal version of [TZ14].
[FT16] Synthesizing Skeletons for Reactive Systems.
With Bernd Finkbeiner
@ATVA 2016.
[FFST16] A Stream-based Specification Language for Network Monitoring.
With Bernd Finkbeiner, Peter Faymonville and Sebastian Schirmer
@RV 2016.
[TZ14] The Complexity of Counting Models of Linear-time Temporal Logic.
With Martin Zimmermann
@FSTTCS 2014.
[FT14] Counting Models of Linear-time Temporal Logic.
With Bernd Finkbeiner
@LATA 2014.

Student Projects

Learning Automata for LTL Valentin Seimetz, Bachelor Thesis, 2017
A Comparison between Lola and QREs Nathalie Zeller, Bachelor Thesis, 2017
FPGA-based Monitoring for Stream Specification Languages Marcel Maltry, Master Thesis, 2017
Optimizing Lola Specifications Mark Timon Hüneberg, Bachelor Thesis, 2015
Approximate LTL Model Counting via Monte Carlo Jennifer Niederländer, Bachelor Thesis, 2015


WiSe 2016/17: Assistant: Seminar: Runtime Verification.
SoSe 2016: Assistant: Embedded Systems.
WiSe 2015/16: Assistant: Seminar: Trends in Software Synthesis.
SoSe 2015: Assistant: Proseminar: Softwarezuverlässigkeit.
WiSe 2014/15: Assistant: Programmierung 1.
SoSe 2014: Advisor: Seminar: Advanced Topics in Infinite Games.
WiSe 2013/14: Assistant: Time Machine.
SoSe 2013: Assistant: Verification.
WiSe 2012/13: Assistant: Automata, Games and Verification.
Advisor: Seminar: Real-time Systems and Synthesis.
SoSe 2010: Tutor: Introduction to Computational Logic.
WiSe 2009/10: Supervision Tutor: Programming 1.
Co-Lecturer: Methodik und Didaktik für Tutoren.
Tutor: Mathematics Pre-Course.
SoSe 2009: Tutor: Concurrent Programming.
WiSe 2008/09: Tutor: Programming 1.
Tutor: Mathematics Pre-Course.