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

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

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.

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

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

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.

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.

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

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

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

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

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

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.

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

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.

We discuss the hierarchy of hyperlogics from a knowledge reasoning perspective

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

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

We study the reactive synthesis problem for hyperproperties.

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.

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

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.

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

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

We study the reactive synthesis problem for hyperproperties.

We study model checking of quantitative hyperproperties.

We present RVHyper, a runtime verification tool for hyperproperties.

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

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

We study the satisfiability problem of HyperLTL.

Updated 04/2023. Website template by Jon Barron.