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.
Contact
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.
Service
I am a member of the program committee for RV 2020.
Publications
| [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 |
Teaching
| 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. |