Christopher Hahn

I am currently employed at Google LLC, where I work as a Senior Research Scientist pioneering next-gen AI solutions for early stage innovations at X, the moonshot factory (formerly known as Google X).

Previously, I served as a Visiting Assistant Professor in the Computer Science Department at Stanford University and an Independent Research Group Leader at the CISPA Helmholtz Center for Information Security.

I earned my Ph.D. (Dr. rer. nat.) at Saarland University, under the supervision of Bernd Finkbeiner.

Email  /  CV  /  Google Scholar  /  Twitter

profile photo

clean-usnob Lightweight Online Learning for Sets of Related Problems in Automated Reasoning
Haoze Wu, C. H., Florian Lonsing, Makai Mann, Raghuram Ramanujan, and Clark Barrett
arXiv preprint, 2023.
arXiv

We present Self-Driven Strategy Learning (sdsl), a lightweight online learning methodology for automated reasoning tasks that involve solving a set of related problems.

clean-usnob Generating Temporal Logical Formulas with Transformer GANs
Jens U. Kreber and C. H.
Neurosymbolic Generative Models (NeSy-GeMs @ ICLR), 2023.
Workshop website.

We consider the scarcity of training data for temporal logics. We summarize a recently performed study on the capabilities of GANs and Wasserstein GANs equipped with Transformer encoders to generate sensible and challenging formulas in the prototypical temporal logic LTL.

clean-usnob nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models
Matthias Cosler, C. H., Daniel Mendoza, Frederik Schmitt, and Caroline Trippel
arXiv preprint, 2023.
arXiv

We present nl2spec, a framework for applying Large Language Models to derive formal specifications from unstructured natural language.

clean-usnob Iterative Circuit Repair Against Formal Specifications
Matthias Cosler, Frederik Schmitt, C. H., and Bernd Finkbeiner
Eleventh International Conference on Learning Representations (ICLR), 2023.
openreview

We present a deep learning approach for repairing sequential circuits against formal specifications.

clean-usnob Formal Specifications from Natural Language
C. H., Frederik Schmitt, Julia J. Tillman, Niklas Metzger, Julian Siber, and Bernd Finkbeiner
arXiv Preprint, 2022.
arXiv

We study the ability of language models to translate natural language into formal specifications with complex semantics. In particular, we fine-tune off-the-shelf language models on three datasets consisting of structured English sentences and their corresponding formal representation.

clean-usnob Temporal Causality in Reactive Systems
Norine Coenen, Bernd Finkbeiner, Hadar Frenkel, C. H., Niklas Metzger, and Julian Siber
20th International Symposium on Automated Technology for Verification and Analysis (ATVA), 2022.
arXiv

We propose an approach to check causality that is tailored to reactive systems, i.e., systems that interact with their environment over a possibly infinite duration.

clean-usnob Explaining Hyperproperty Violations
Norine Coenen, Raimund Dachselt, Bernd Finkbeiner, Hadar Frenkel, C. H., Tom Horak, Niklas Metzger, and Julian Siber
34th International Conference on Computer-Aided Verifciation (CAV), 2022.
arXiv

We present an explanation method for counter examples to hyperproperties described in the specification logic HyperLTL.

clean-usnob Attention Flows for General Transformers
Niklas Metzger, C. H., Julian Siber, Frederik Schmitt, and Bernd Finkbeiner
arXiv Preprint, 2022
arXiv

We study the computation of how much an input token in a Transformer model influences its prediction.

clean-usnob Visual Analysis of Hyperproperties for Understanding Model Checking Results
Tom Horak, Norine Coenen, Niklas Metzger, C.H., Tamara Flemisch, Julián Méndez, Dennis Dimov, Bernd Finkbeiner, and Raimund Dachselt
IEEE Transactions on Visualization and Computer Graphics (VIS), 2022.
arXiv / online tool / project page

We introduce HyperVIS, which is a online tool that provides interactive visualizations of a given system model, specification, and counterexample to a hyperproperty.

clean-usnob Generating Symbolic Reasoning Problems with Transformer GANs
Jens U. Kreber and C.H.
arXiv Preprint, 2021.
arXiv

We study the capabilities of GANs and Wasserstein GANs equipped with Transformer encoders to generate sensible and challenging training data for symbolic reasoning domains.

clean-usnob Neural Circuit Synthesis from Specification Patterns
Frederik Schmitt, C.H., Markus N. Rabe, and Bernd Finkbeiner
35th Conference on Neural Information Processing Systems (NeurIPS), 2021.
arXiv / GitHub

We train hierarchical Transformers on the task of synthesizing hardware circuits directly out of high-level logical specifications in linear-time temporal logic.

clean-usnob Deep Learning for Temporal Logics
Frederik Schmitt, C.H., Jens U. Kreber, Markus N. Rabe, and Bernd Finkbeiner
6th Conference on Artificial Intelligence and Theorem Proving (AITP), 2021.

We report on current advances in applying deep learning to temporal logical reasoning tasks, showing that models can even solve instances where competitive classical algorithms timed out.

clean-usnob Runtime Enforcement of Hyperproperties
Norine Coenen, Bernd Finkbeiner, C.H., Jana Hofmann, and Yannick Schillo
The 19th International Symposium on Automated Technology for Verification and Analysis (ATVA), 2021
arXiv / talk (start at 31:00) / GitHub

We study enforcement algorithms for specifications given as formulas in universally quantified HyperLTL.

clean-usnob Teaching Temporal Logics to Neural Networks
C.H., Frederik Schmitt, Jens U. Kreber, Markus N. Rabe, and Bernd Finkbeiner
Ninth International Conference on Learning Representations (ICLR), 2021.
arXiv / talk / poster / GitHub

We study two fundamental questions in neuro-symbolic computing: can deep learning tackle challenging problems in logics end-to-end, and can neural networks learn the semantics of logics.

clean-usnob The Hierarchy of Hyperlogics: A Knowledge Reasoning Perspective
Norine Coenen, Bernd Finkbeiner, C.H., and Jana Hofmann
17th International Conference on Principles of Knowledge Representation and Reasoning (KR), Recently published research track, 2020.
talk (by Jana Hofmann)

We discuss the hierarchy of hyperlogics from a knowledge reasoning perspective

clean-usnob Realizing ω-regular Hyperproperties
Bernd Finkbeiner, C.H., Jana Hofmann, and Leander Tentrup
32nd International Conference on Computer-Aided Verification (CAV), 2020.
arXiv

We study the expressiveness and reactive synthesis problem of HyperQPTL, a logic that specifies ω-regular hyperproperties.

clean-usnob Efficient monitoring of hyperproperties using prefix trees
Bernd Finkbeiner, C.H., Marvin Stenger, Leander Tentrup
International Journal on Software Tools for Technology Transfer (STTT), 2020.
Special Issue of TACAS 2018 / arXiv

We present the monitoring approach implemented in the latest version of RVHyper, a runtime verification tool for hyperproperties.

clean-usnob Synthesis from Hyperproperties (extended journal version)
Bernd Finkbeiner, C.H., Philip Lukert, Marvin Stenger, and Leander Tentrup
Acta Informatica, 2019
Special Issue on SYNT 2018

We study the reactive synthesis problem for hyperproperties.

clean-usnob Algorithms for Monitoring Hyperproperties (tutorial)
C. H.
3rd Wold Congress on Formal Methods: 19th International Conference on Runtime Verification (RV), 2019.
tutorial slides

In this tutorial, we summarize recent algorithmic advances in monitoring hyperproperties from logical specifications. We classify current approaches into two classes: combinatorial approaches and constraint-based approaches.

clean-usnob Monitoring Hyperproperties (extended journal version)
Bernd Finkbeiner, C. H., Marvin Stenger, and Leander Tentrup
Formal Methods in System Design (FMSD)
Special Issue on Runtime Verification 2017

We investigate the runtime verification problem of HyperLTL formulas for three different input models: The parallel, the bounded sequential and the unbounded sequential model.

clean-usnob The Hierarchy of Hyperlogics
Norine Coenen, Bernd Finkbeiner, C.H., and Jana Hofmann
34th Annual ACM/IEE Symposium on Logic in Computer Science (LICS), 2019.
arXiv

We study the expressive power across the spectrum of linear-time and branching-time hyperlogics. Within the hierarchy of hyperlogics, we identify new boundaries on the decidability of the satisfiability problem.

clean-usnob Constraint-based Monitoring of Hyperproperties
C. H., Marvin Stenger, and Leander Tentrup
25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2019.
arXiv / poster

We monitor hyperproperties by rewriting a formula in the temporal logic HyperLTL to a Boolean constraint system.

clean-usnob MGHyper: Checking Satisfiability of HyperLTL formulas beyond the Exists*-Forall* Fragment
Bernd Finkbeiner, C. H., and Tobias Hans
International Symposium on Automated Technology for Verification and Analysis (ATVA), 2018.
arXiv

We introduce MGHyper, a tool for automatic satisfiability checking and model generation for hyperproperties beyond the decidable Exists*-Forall* fragment of HyperLTL.

clean-usnob Synthesizing Reactive Systems from Hyperproperties
Bernd Finkbeiner, C. H., Philip Lukert, Marvin Stenger, and Leander Tentrup
30th International Conference on Computer Aided Verification (CAV), 2018.
arXiv / tool page / GitHub

We study the reactive synthesis problem for hyperproperties.

clean-usnob Model Checking Quantitative Hyperproperties
Bernd Finkbeiner, C. H., and Hazem Torfah
30th International Conference on Computer Aided Verification (CAV), 2018.
arXiv

We study model checking of quantitative hyperproperties.

clean-usnob RVHyper: A Runtime Verification Tool for Temporal Hyperproperties
Bernd Finkbeiner, C. H., Marvin Stenger, and Leander Tentrup
17th International Conference on Runtime Verification (RV), 2017.
arXiv / tool page / GitHub / poster

We present RVHyper, a runtime verification tool for hyperproperties.

clean-usnob Monitoring Hyperproperties
Bernd Finkbeiner, C. H., Marvin Stenger, and Leander Tentrup
17th International Conference on Runtime Verification (RV), 2017.
arXiv / slides

We investigate the runtime verification problem of HyperLTL formulas for three different input models: The parallel, the bounded sequential and the unbounded sequential model.

clean-usnob EAHyper: Satisfiability, Implication and Equivalence Checking of Hyperproperties
Bernd Finkbeiner, C. H., Marvin Stenger
29th International Conference on Computer-Aided Verification (CAV), 2017.
tool page / GitHub / slides

We introduce EAHyper, the first satisfiability solver for hyperproperties expressed in the decidable fragment of HyperLTL.

clean-usnob Deciding Hyperproperties
Bernd Finkbeiner, C. H.
27th International Conference on Concurrency Theory (CONCUR), 2016.
arXiv / slides

We study the satisfiability problem of HyperLTL.


Updated 04/2023. Website template by Jon Barron.