Forschung

Der Lehrstuhl beschäftigt sich mit einer Vielzahl von Themen aus dem Bereich Formale Logik und Verifikation, unter anderem:

• Eigenschaften von logischen Fragmenten und Theorien
• Kalküle und effektive Beweis- oder Entscheidungsprozeduren, implementiert in Form vom SMT Solvern
• Methoden für Craig Interpolation und Quantorenelimination
• Automatenmethoden
• Spezifikations- und Zwischensprachen für die Verifikation