Jan-Christoph Kassing

Jan-Christoph Kassing

(Probabilistic) Program Verification, Rewriting, Termination

Jan-Christoph Kassing

I have been a research assistant and PhD student in the Research Group “Pro­gram­ming Languages and Verification” headed by Professor Jürgen Giesl since October 2022 and one of the main developers of the Automated Program Verification Environment (AProVE) tool. Moreover, I am part of the interdisciplinary Research Training Group UnRAVeL.

Personal Research: My research focuses on theoretical computer science. I’m interested in automated reasoning and verification of (probabilistic) programs. In particular, I work on fully automated termination and complexity analysis of functional programs dealing with data structures. For this, I focus on analyzing termination and (expected) complexity of (probabilistic) term rewriting, which is a very basic functional programming language. All my contributions are implemented in the Automated Program Verification Environment (AProVE) Tool.

AProVE: AProVE is a system for automated termination and complexity proofs of term rewrite systems (TRSs) and several variations of TRSs. Moreover, AProVE also handles several other formalisms, e.g., imperative programs (Java Bytecode and C / LLVM), functional programs (Haskell 98), and logic programs (Prolog). The power of AProVE is demonstrated in the annual International Competition of Termination Tools and the International Competition on Software Verification. AProVE also won two Kurt Gödel medals at VSL 2014.

UnRAVeL: UnRAVeL (UNcertainty and Randomness in Algorithms, VErification and Logic) is an interdisciplinary Research Training Group funded by the German Research Foundation (DFG). The goal is to significantly advance probabilistic modelling and analysis for uncertainty by developing new theories, algorithms, and tool-supported verification techniques, and to apply them to core problems of security, planning, and safety and performance analysis. To tackle these research challenges, theoretical computer scientists from computer-aided verification, logic and games, algorithms and complexity, together with experts from management science, and railway engineering form the core of this Research Training Group.