Christopher Hahn
Contact
Phone: +49 681 302 5664
eMail: christopher dot hahn at cispa dot de
About me
I was a Ph.D. student in the Reactive Systems Group at the Computer Science Department at Saarland University.
I defended my thesis “Logical and Deep Learning Methods for Temporal Reasoning” in December, 2021 and joined the CISPA-Stanford Center. Please find my new homepage here: christopherhahn.io.
Publications
Teaching Temporal Logics to Neural Networks
With Frederik Schmitt, Jens U. Kreber, Markus N. Rabe, and Bernd Finkbeiner.Ninth International Conference on Learning Representations (ICLR 2021).
The Hierarchy of Hyperlogics: A Knowledge Reasoning Perspective
With Norine Coenen, Bernd Finkbeiner and Jana Hofmann.17th International Conference on Principles of Knowledge Representation and Reasoning, Recently Published Research Track (KR 2020).
Realizing omega-regular Hyperproperties
With Bernd Finkbeiner, Jana Hofmann, and Leander Tentrup.32nd International Conference on Computer-Aided Verification (CAV 2020).
Efficient monitoring of hyperproperties using prefix trees
With Bernd Finkbeiner, Marvin Stenger, and Leander Tentrup.International Journal on Software Tools for Technology Transfer, TACAS 2018 Special Issue (STTT 2020).
Synthesis from Hyperproperties
With Bernd Finkbeiner, Philip Lukert, Marvin Stenger, and Leander Tentrup.Acta Informatica.
Monitoring Hyperproperties
With Bernd Finkbeiner, Marvin Stenger and Leander Tentrup.Formal Methods in System Design (FMSD).
The Hierarchy of Hyperlogics
With Norine Coenen, Bernd Finkbeiner and Jana Hofmann.34th Annual ACM/IEE Symposium on Logic in Computer Science (LICS 2019).
Constraint-based Monitoring of Hyperproperties
With Marvin Stenger and Leander Tentrup.25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019).
MGHyper: Checking Satisfiability of HyperLTL formulas beyond the ∃* ∀* Fragment.
With Bernd Finkbeiner and Tobias Hans.16th International Symposium on Automated Technology for Verification and Analysis (ATVA 2018).
Synthesizing Reactive Systems from Hyperproperties.
With Bernd Finkbeiner, Philip Lukert, Marvin Stenger and Leander Tentrup.30th International Conference on Computer-Aided Verification (CAV 2018).
Model Checking Quantitative Hyperproperties.
With Bernd Finkbeiner and Hazem Torfah.30th International Conference on Computer-Aided Verification (CAV 2018).
RVHyper: A Runtime Verification Tool for Temporal Hyperproperties.
With Bernd Finkbeiner, Marvin Stenger, and Leander Tentrup.24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2018).
Tool. Poster.
Monitoring Hyperproperties.
With Bernd Finkbeiner, Marvin Stenger, and Leander Tentrup.17th International Conference on Runtime Verification (RV 2017).
Deciding Hyperproperties.
With Bernd Finkbeiner.27th International Conference on Concurrency Theory (CONCUR 2016).
Tools
A Runtime Verification Tool for Temporal Hyperproperties.
With Marvin Stenger and Leander Tentrup.Satisfiability, Implication, and Equivalence Checking of Hyperproperties.
With Marvin Stenger.Scientific Service
- PC member for IJCAI’21
- Reviewer for STTT’20
- Subreviewer for LICS’19, ATVA’19, CSL’20, CONCUR’20, LICS’21, CAV’21
Presentations
- Monitoring Hyperproperties: Slides
at 17th International Conference on Runtime Verification in Seattle, USA, September 2017. - EAHyper: Satisfiability, Implication, and Equivalence Checking of Hyperproperties: Slides
at 29th International Conference on Computer Aided Verification in Heidelberg, Germany, July 2017. - Deciding Hyperproperties: Slides
at Highlights of Logic, Games and Automata in Brussels, Belgium, September 2016. - Deciding Hyperproperties: Slides
at the 27th International Conference on Concurrency Theory in Quebec, Canada, August 2016.
Theses
- Satisfiability and Monitoring of Hyperproperties Master Thesis 2017
- Deciding HyperLTL Bachelor Thesis 2016
Student Projects
Ongoing
- Tobias Hans, tbd, Master Thesis
Completed
- Matthias Cosler, “Towards Synthesizing Smart Contracts: Reducing ATL* Synthesis to HyperLTL Synthesis”, Bachelor Thesis (co-advised by Jana Hofmann)
- Jens Heinen, Model Checking Timed Hyperproperties, Master Thesis 2018
- Philip Lukert, HyperLTL Synthesis, Bachelor Thesis 2018
- Tobias Hans, MGHyper: Checking Satisfiability of HyperLTL formulas beyond the ∃*-∀*-Fragment, Bachelor Thesis 2018
Teaching Videos
- Programming 1 at Saarland University: YouTube-Channel (with Jana Hofmann, in German).
- Mathematics Precourse at Saarland University: YouTube-Channel (in German).
Teaching
| Summer 2019 | Advisor for Softwarezuverlässigkeit at the Reactive Systems Group |
| Winter 2018/2019 | Advisor for Hyperproperties at the Reactive Systems Group. |
| Summer 2018 | Advisor for Formal Verification of Security Protocols at the Reactive Systems Group. |
| Winter 2017/2018 | Teaching Assistant for Programming 1 at the Reactive Systems Group. received the Busy Beaver award for outstanding teaching performance |
| Summer 2017 | Lecturer for Mathematics Precourse at Saarland University received the BESTE award for student initiatives and extraordinary commitment |
| Winter 2016/2017 | Teaching Assistant for Verification at the Reactive Systems Group. |
| Summer 2016 | Lecturer and Coach for Mathematics Precourse at Saarland University |
| Summer 2016 | Student TA for Concurrent Programming at the Dependable Systems and Software Chair. |
| Winter 2015/2016 | Organizer of Didactic Seminar for Re-exam Student TAs |
| Winter 2015/2016 | Supervision Student TA for Programming 1 at the Programming Systems Lab. |
| Summer 2015 | Coach for Mathematics Precourse at Saarland University. |
| Winter 2014/2015 | Organizer of Didactic Seminar for Re-exam Student TAs |
| Winter 2014/2015 | Student TA for Programming 1 at the Reactive Systems Group. |
| Summer 2014 | Student TA for Mathematics Precourse at Saarland University. |
| Winter 2013/2014 | Re-exam Student TA for Programmierung 1 at the Dependable Systems and Software Chair. |