Niklas Metzger
Contact
Niklas Metzger
Reactive Systems Group
CISPA Helmholtz Center for Information Security
Phone: +49 681 87083 2471
eMail: niklas.metzger at cispa.de
Building: E 9.1 Room: 1.09
About me
I am a Ph.D. student at CISPA Helmholtz Center for Information Security and Saarland University.
I am interested in hyperproperties, reactive synthesis, and the interplay of formal methods and machine learning. My research currently focuses on compositional synthesis guided by the principles of knowledge, actual causality for reactive systems, and building machine learning models as heuristics in complex formal method tasks.
News
- I am co-organizing HYPER24 together with Hadar Frenkel and Hazem Torfah. The workshop will be part of CAV24. Check out the website for more information!
- Our paper Monitoring Second-Order Hyperproperties will appear at AAMAS 2024!
- I am a meber of the artefact evaluation committee for TACAS24.
- The blogpost for our paper Second-Order Hyperproperties is online!
Publications
| to appear | Information Flow Guided Synthesis with Unbounded Communication. With Bernd Finkbeiner and Yoram Moses. 36th International Conference on Computer-Aided Verification (CAV 2024). July 2024 |
| to appear | Synthesis of Temporal Causality. With Bernd Finkbeiner, Hadar Frenkel, and Julian Siber. 36th International Conference on Computer-Aided Verification (CAV 2024). July 2024 |
| [BFFM24] | Monitoring Second-Order Hyperproperties. With Raven Beutner, Bernd Finkbeiner, and Hadar Frenkel. 23rd International Conference on Autonomous Agents and Multi-Agent Systems (AAMAS 2024), to appear. |
| [CFF+23] | Second-Order Hyperproperties. With Raven Beutner, Bernd Finkbeiner, and Hadar Frenkel. 35th International Conference on Computer-Aided Verification (CAV 2023) |
| [CFF+22] | Temporal Causality in Reactive Systems. With Bernd Finkbeiner, Hadar Frenkel, Christopher Hahn, and Julian Siber. 20th International Symposium on Automated Technology for Verification and Analysis (ATVA 2022) |
| [FMM22] | Information Flow Guided Synthesis. With Bernd Finkbeiner and Yoram Moses. 34th International Conference on Computer-Aided Verification (CAV 2022). August 2022 |
| [CDF+22] | Explaining Hyperproperty Violations. With Norine Coenen, Raimund Dachselt, Bernd Finkbeiner, Hadar Frenkel, Christopher Hahn, Tom Horak, and Julian Siber. 34th International Conference on Computer-Aided Verification (CAV 2022) |
| [FP22] | Live synthesis. With Bernd Finkbeiner and Felix Klein Innovations in Systems and Software Engineering, ATVA 2021 Special Issue (ISSE 2022) |
| [HCM+21] | Visual Analysis of Hyperproperties for Understanding Model Checking Results. With Tom Horak, Norine Coenen, Christopher Hahn, Tamara Flemisch, Julián Méndez, Dennis Dimov, Bernd Finkbeiner, and Raimund Dachselt IEEE VIS Visualization & Visual Analytics (VIS 2021) |
| [FKM21] | Live Synthesis. With Bernd Finkbeiner and Felix Klein. International Symposium on Automated Technology for Verification and Analysis (ATVA 2021) |
| [HM19] | Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems. With Jesko Hecking-Harbusch. International Symposium on Automated Technology for Verification and Analysis (ATVA 2019) |
| Preprints | |
| [HSTMSF22] | Formal Specifications from Natural Language. With Christopher Hahn, Frederik Schmitt, Julian Siber, Julia J. Tillman, and Bernd Finkbeiner. |
| [MHSSF22] | Attention Flows for General Transformers With Christopher Hahn, Julian Siber,Frederik Schmitt, and Bernd Finkbeiner. |
| [MSS22] | Conservative Hybrid Automata from Development Artifacts With Maximilian Schwenger and Sanny Schmitt. |
Presentations
- Compositional Synthesis with Hyperproperties at Dagstuhl Seminar The Futures of Reactive Synthesis
- Information-Flow Guided Synthesis at 35th International Conference on Computer-Aided Verification (CAV 2022). August 2022, Haifa, Israel
- Live Synthesis: Talk at 19th International Symposium on Automated Technology for Verification and Analysis in Gold Coast, Australia, October 2021.
- Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems: Slides
at 17th International Symposium on Automated Technology for Verification and Analysis in Taipei, Taiwan, October 2019.
Scientific Service
- Member of the Artefact Evaluation Committee at CAV’23 and TACAS’24
- Subreviewer for ATVA’20, RV’20, TACAS’20, ATVA’21, CONCUR’21, CAV’21, TACAS21, CAV’22, ATVA’22, CAV’23, ATVA’23, DATE’24, STACS’24, LICS’24, CAV’24
Student Projects
| TBD | Ivo Bakowsky, Bachelor Thesis |
| Monitor-Assisted Hybrid Model Refinement | Stefan Oswald, Master Thesis (co-advised by Maximilian Schwenger and Julia Wichlacz) |
| Complete Bounded Model Checking for Hyperproperties | Florian Bies, Bachelor Thesis (co-advised by Norine Coenen) |
| Evaluation of Vulnerabilities of a Lane Keeping Assist System based on Simulations | Jonas Birtel, Bachelor Thesis (in cooperation with BSI) |
| Predicting Timed Traces with Neural Networks | Ayham Omar, Bachelor Thesis (co-advised by Christopher Hahn) |
Teaching
| Summer 2022 | Seminar Advisor for Neural-Symbolic Computing. |
| Summer 2021 | Assistant for Software Reliability |
| Summer 2020 | Seminar Advisor for Neural-Symbolic Computing. |
| Summer 2019 | Lecturer for Programmierung 2 Precourse at Saarland University |
| Summer 2018 | Supervising Teaching Assistant for Programmierung 2 at Saarland University |
| Summer 2017 | Supervising Teaching Assistant for Programmierung 2 at Saarland University |
| Summer 2016 | Teaching Assistant for Programmierung 2 at Saarland University |
Theses
| Live Synthesis | Master Thesis, Saarland University, 2019 |
| Bounded Synthesis of Petri Games with True Concurrecy Firing Semantics | Bachelor Thesis, Saarland University, 2017 |