Christopher Hahn

I am a Visiting Assistant Professor in Computer Science at Stanford University, where I work in the intersection between deep learning and formal methods. Currently, I am especially interested in the autoformalization of mathematics and logics.

Previously, I completed my PhD (Dr. rer. nat.) at Saarland University, where I was fortunate to be advised by Bernd Finkbeiner.

Email  /  Bio  /  CV  /  Google Scholar  /  Twitter

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 02/2022. Website template by Jon Barron.