Head

Research Group Leaders

Yasmine Briefs
Tobias Gehl
Johanna Meerjanssen

Fajar Haifani (Ph.D. 2023): On a Notion of Abduction and Relevance for First-Order Logic Clause Sets

Mathias Fleury (Ph.D. 2020): Formalization of Logical Calculi in Isabelle/HOL

Martin Bromberger (Ph.D. 2019): Decision Procedures for Linear Arithmetic

Marco Voigt (Ph.D. 2019): Decidable Fragments of First-Order Logic and of First-Order Linear Arithmetic with Uninterpreted Predicates

Andreas Teucke (Ph.D. 2018): An Approximation and Refinement Approach to First-Order Automated Reasoning

Ching Hoo Tang (Ph.D. 2017): Logics for Rule-Based Configuration Systems

Daniel Wand (Ph.D. 2017): Superposition: Types and Induction

Marek Kosta (Ph.D. 2016): New Concepts for Real Quantifier Elimination by Virtual Substitution

Noran Azmy (Ph.D. 2016): A Machine–Checked Proof of Correctness of Pastry

Martin Suda (Ph.D. 2015): Resolution-based methods for linear temporal reasoning

Manuel Lamotte-Schubert (Ph.D. 2015): Automatic Authorization Analysis

Willem Hagemann (Ph.D. 2015): Symbolic Orthogonal Projections: A New Polyhedral Presentation for Reachability Analysis of Hybrid Systems

Arnaud Fietzke (Ph.D. 2014): Labelled Superposition

Tianxiang Lu (Ph.D. 2013): Formal Verification of the Pastry Protocol

Evgeny Kruglov (Ph.D. 2013): Superposition Modulo Theory

Patrick Wischnewski (Ph.D. 2012): Efficient Reasoning Procedures for Complex First-Order Theories

Carsten Ihlemann (Ph.D. 2010): Reasoning in Combinations of Theories

Matthias Horbach (Ph.D. 2010): Saturation-Based Decision Procedures for Fixed Domain and Minimal Model Validity

Swen Jacobs (Ph.D. 2010): Hierarchic Decision Procedures for Verification

Thomas Hillenbrand (Ph.D. 2009): Superposition and Decision Procedures Back and Forth