Earlier Seminar Reports

WS 2017

• Christina Kohl
  ProTeM
• Alexander Lochmann
  AC Compatible Simplification Orders
• Florian Meßner
  Conditional Nonreachability with Tree Automata
• Julian Parsert
  Formalization of Social Choice Theory

SS 2017

• Bojan Cvjetkovic
  Cutting Planes for Solving Integer Programs
• Martin Hartl
  SAT Encodings of Pseudo-Boolean Constraints (2)
• Philipp Wirtenberger
  Efficient Characterisation of Polynomially Bounded Matrices

WS 2016

• Bojan Cvjetkovic
  Certification of Linear Ranking Functions
• Martin Hartl
  SAT Encodings of Pseudo-Boolean Constraints
• Philipp Wirtenberger
  Polynomially Bounded Matrix Interpretations

SS 2016

• David Kofler
  Efficiently Checking Equivalence of Nondeterministic Finite Automata
• Manuel Schneckenreither
  Amortized Resource Analysis for Term Rewrite Systems

SS 2015

• Sebastian Mayr
  Certified Match-Bounds with Witnesses
• Andrew Morris
  Proving with Dependent Types
• Alexander Maringele
  Instantiation-Based Theorem Prover meets Maximal Completion
• Franziska Rapp
  (Un)decidability of the First-Order Theory of One-Step Rewriting
• Manuel Schneckenreither
  Amortized Resource Analysis meets Term Rewrite Systems

WS 2014

• Sebastian Mayr
  Match-Bounds
• Andrew Morris
  Towards an Isabelle Formalisation of the Cayley-Hamilton Theorem
• David Obwaller
  Interaction Nets with Nested Pattern Matching
• Franziska Rapp
  Automatically Finding Ground Rewrite Systems

SS 2014

• Andreas Kochesser
  Monotonicity Constraint Transition Systems
• Josef Lindsberger
  From Finite Linear CSP to SAT
• Alexander Maringele
  Instantiation-based Theorem Proving with Equality
• David Obwaller
  Interaction Combinators and Hard Combinators

WS 2014

• Michael Färber
  Calculating Norms of Simple Deterministic Grammars
• Andreas Kochesser
  Constraint Transition Systems
• Josef Lindsberger
  Constraint Satisfiability to Boolean Satisfiability
• Maria Schett
  Towards Complexity of Graph Rewriting

SS 2013

• Florian Hagenauer
  Formalization of Virtual Traffic Lights
• Maria Schett
  Answer Set Programming

WS 2012

• Benjamin Höller
  Confluence of Rewrite Systems with AC Rules (2)

SS 2012

• Michael Färber
  Constructive Type Theory and dependent types in Isabelle
• Benjamin Höller
  Confluence of Rewrite Systems with AC Rules
• Michael Schaper
  Bound Analysis of Imperative Programs

WS 2011

• Simon Legner
  Non-Linear Arithmetic – SAT Modulo Linear Arithmetic for Solving Polynomial Constraints
• Julian Nagele
  Higher-Order Dependency Pairs
• Michael Schaper
  Deciding the Complexity of Programs Automatically – Termination Graphs Revisited

SS 2011

• Simon Legner
  Non-Linear Arithmetic
• Julian Nagele
  Higher-Order Recursive Path Order
• Thomas Sternagel
  Automatic Proofs in Equational Logic (2)

WS 2010

• Thomas Sternagel
  Automatic Proofs in Equational Logic

SS 2009

• Martin Hammerer
  Satisfiability Games for CTL

WS 2008

• Matthias Gander
  Supercubing
• Martin Hammerer
  Satisfiability Games for LTL

SS 2008

• Martin Avanzini
  Calculating Polynomial Runtime Properties
• Stefan Kopeinig
  Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL
• Philipp Ruff
  Clause Learning in SAT Solving 2

WS 2007

• Martin Avanzini
  mwp-Bounds for Complexity Analysis
• Matthias Gander
  Symmetry Breaking in SAT Solving
• Philipp Ruff
  Clause Learning in SAT Solving
• Caroline Terzer
  Pseudo Boolean Constraint Solving 2
• Sarah Winkler
  From DPLL to DPLL(T)