Michael Krawez: "Model Generation in Local Theory Extensions and Applications to Verification", 2012
Miguel Angel Molina Hernandes: "Algorithmen zur Überprüfung der Erfüllbarkeit in Fragmenten der Linearen Arithmetik", 2014
Anais Böttcher: "Die Verikation von Sicherheitseigenschaften von Systemen von Fahrzeugen", 2016
Sven Christoph: "Formal Verification of Safety of Acceleration Behavior in Automated Driver Assistance Systems", 2017
Sebastian Thunert: "Anwendung von Symbolelimination in Theorieerweiterungen", 2017
Julius Wild: "Visualisation of Scenarios for Autonomous Driving", 2018
Jamal Droßard: "Automated proving of topological theorems using encodings in modal logics", 2018
Matthias Becker: "Implementierung und Verifikation von Sicherheitseigenschaften autonomen Fahrens mit Lego Mindstorms". 2019
Fabian Bell: "Comparison of Approaches for Invariant Generation". 2019
Kevin Weirauch: "Automatische Beweise in der Mengenlehre und deren Anwendungen in Mathematik und Verifikation" . 2020
Philipp Marohn: "Verifikation und Generierung von Constraints in parametrisierten Systemen", 2021
Tim Merker: "Toolkit für automatisches Beweisen und Symbolelimination durch geordnete Resolution", 2021
Fabian Maxeiner: "Verifikation von Sicherheitseigenschaften für lineare, hybride Automaten", 2021
Timothy Gillespie: "Applied Constraint Generation on Parameters of Recursive Functions and Data Structures for Structural Induction Proofs", 2022
Mike Wickert: "Toolkit für den aussagenlogischen Tableaukalkül", 2023
Valerie Simon: "Automatisches Beweisen in der geometrischen Graphentheorie", 2024
Jan Denzer: "Axiom-Pinpointing und alternative Verfahren zur Erklärung von Subsumtionsbeziehungen in Beschreibungslogiken", 2024
MSc Theses:
Daniel Heck: "Automatisches Beweisen mittels Gröbnerbasen in der Geometrie", 2014
Irina Karpova: "Craig Interpolation in UTVPI", 2015
Dennis Peuter: "Automatisches Beweisen in der analytischen Geometrie", 2016
Sebastian Thunert: "Automatization of Computing High-Level Explanations for Subsumptions in EL and EL+", 2021
Katarina Miller: "Automatisierung von automatischen Beweisen in der analytischen Geometrie", 2023
Kevin Weirauch: "Automated Reasoning in Local Theory Extensions", 2023
Tim Merker: "Specification and Verification of Autonomous Vehicles in a Road Blockade", 2023
Vivien Laszlo: 2024 (ongoing, advised together with Matthias Thimm)
Fabian Maxeiner: 2024
PhD Theses:
Swen Jacobs: "Hierarchic Reasoning in Verification", 2009
Carsten Ihlemann: "Reasoning in Combinations of Theories", 2010
Markus Bender (ongoing)
Dennis Peuter: "Applications for Symbol Elimination in Combination with Hierarchical Reasoning”, 2024
Lucas Böltz (ongoing)
Further Topics
We have various topics for BSc, MSc and PhD theses.
If you are interested in writing a thesis in the group, just contact us.
Area:Study theories for which complete instantiation method exists:
Most of the algorithms for checking satisfiability modulo theories were devised for being used for ground formulae. Therefore, the state-of-the-art SMT solvers with support for quantifiers use heuristics for quantifier instantiation. Such heuristics are in general sound but incomplete: if a contradiction is derived after instantiating a set N of clauses, then N is clearly unsatisfiable. However, if no contradiction can be derived after instantiation we do not know anyting about the satisfiability of N (it could happen that not all instantiations needed for deriving a contradiction were considered). It is therefore important to identify classes of theories for which complete instantiation methods exists, i.e. in which we can characterize the set of instances which are necessary and sufficient for deriving a contradiction in case of unsatisfiability. The advantage of having a complete instantiation method is that if unsatisfiability cannot be derived from the set of instances of N, we have the guarantee that the set N of quantified clauses is satisfiable. In fact, we often can effectively construct a model of N from a model of its set of instances.
Topics for PhD theses are available in the following areas:
Automated reasoning and applications
Verification (reactive and real time systems/hybrid systems)
Ontologies/description logics
If you are interested in a thesis in one of the areas above (or inrelated areas) please contact Viorica Sofronie-Stokkermans
Topics for BSc and/or MSc theses:
1. Recognize theories with complete instantiation
The goal is to obtain systematic ways of recognizing theories for which complete instantiation methods exist:
Semantic criteria
Syntactic criteria (automatically recognize formulae in the array property fragment; pointer fragment, boundedness, monotonicity, ...)
Other criteria (to be discussed)
Saturation under ordered resolution
and to use these results for systematically investigating the complete instantiation schemata for classes of theories.
Remark: Topics 1 and 2 can be considered together (for a BSc/MSc thesis)
2. Model generation
Starting from a theory for which a complete instantiation schema is known, we would like to obtain ways of constructing models for satisfiable sets of (quantified) formulae. The challenge here would be to obtain means of synthetically and finitely representing potentially infinite models. Such examples can be used as counterexamples e.g, in mathematics, or as examples of systems with undesired unsafe behavior, for instance in verification.
Remark: Topics 1 and 2 can be considered together (for a BSc/MSc thesis)
3. Parametric verification and quantifier elimination
The hierarchical reasoning method in theory extensions which we proposed, allows not only to check the satisfiability of a given set of constraints. We can also consider parametric problems (in which some of the constants which appear can be considered to be parametric) and generate constraints on the parameters which guarantee the satisfiability/unsatisfiability of certain formulae. This is extremely useful e.g. in program verification and design, as well the verification and design of parametric real time or hybrid systems.
4. Programming project
Reasoning in extensions and combinations of theories and applications (logic, verification, databases)
5. Programming project: Interpolant generation
Interpolants are explanations for unsatisfiability of conjunctions of formulae A, B containing only logical symbols used in both A and B;they are nowadays widely used in verification and databases. We identified ways for efficiently computing interpolants in various theories. The goal of this project/thesis is to implement these methods.
6. Automated reasoning and graph theory
7. Description logics (especially the tractable description logic EL): Theory and applications
