EN | DE
Theoretische Informatik

This is an old revision of the document!


Themen für Studentische Arbeiten

Wenn Sie eine Bachelor-, Master-, Studien-, Projekt- oder Diplomarbeit bei der Theoretischen Informatik machen wollen, sind Sie hier richtig.

Sie können die Mitarbeiter auch direkt zu Themen ansprechen (wenn Sie beispielsweise einen konkreten anderen Themenwunsch haben).


Prof. Lutz Schröder's proposals


Fuzzy Description Logic

In der unscharfen Logik (Fuzzy Logic) werden die klassischen Wahrheitswerte “wahr”/“falsch” ersetzt durch Wahrheitsgrade, typischerweise Zahlen zwischen 0 und 1. Über den ursprünglich rein propositionalen Formalismus hinaus gibt es mittlerweile ausdrucksstarke unscharfe Logiken; eine interessante Klasse noch entscheidbarer Logiken dieser Art sind die unscharfen Beschreibungslogiken (Fuzzy Description Logics). Effiziente Deduktionsalgorithmen für Fuzzy DLs werden gerade erst entwickelt, wie etwa dieser hier. Es liegt bereits eine Implementierung eines Tableaualgorithmus für fuzzy ALC vor; mögliche weitere Themen betreffen die systematische Optimierung des Algorithmus und die Erweiterung auf ausdrucksstärkere Logiken.

Art der Arbeit: Bachelor- oder Masterarbeit

Ansprechpartner: Lutz Schröder


Leichtgewichtige Beschreibungslogik

Leichtgewichtige Beschreibungslogiken zeichnen sich durch geringe Ausdrucksstärke bei gleichzeitiger effizienter Entscheidbarkeit der zentralen Schlussfolgerungsprobleme aus. Die zur Zeit vielleicht erfolgreichste leichtgewichtige Beschreibungslogik ist EL, das auch die in wichtigen großen Ontologien wie SNOMET CT verwendet wird. Wir haben eine koalgebraische Verallgemeinerung von EL entwickelt, in der statt der üblichen relationalen Modalitäten auch z.B. verschiedene spielorientierte Modalitäten verwendet werden können. Ein Reasoner für koalgebraisches EL ist in Vorarbeiten bereits implementiert worden. Als weitere Arbeiten bieten sich systematische Evaluationen sowie eine Erweiterung sowohl der Theorie als auch der Implementierung auf sogenannte general concept inclusions an.

Art der Arbeit: Bachelor- oder Masterarbeit

Ansprechpartner: Lutz Schröder


Koalgebraisches T

Koalgebraische Modallogik dient als allgemeines Rahmenwerk für Modallogiken jenseits der relationalen Welt, z.B. für probabilistische oder spieltheoretische Modalitäten. Die meisten Resultate in der koalgebraischen Modallogik haben als Gültigkeitsbereich ausschließlich solche Logiken, die, ähnlich wie die Beschreibungslogik ALC bzw. die relationale Modallogik K, nur durch sogenannte Rang-1-Axiome, also solche, in denen alle aussagenlogischen Variablen unter genau einer Modalität stehen, definiert sind (im Falle von K lautet das Axiom [](a→b) → []a → []b). In diesem Projekt soll die Allgemeinheitsebene auf solche Axiome angehoben werden, in denen zwar noch keine geschachtelten Modalitäten, wohl aber Vorkommen von aussagenlogischen Variablen außerhalb von Modaloperatoren erlaubt sind; Grundbeispiel hierfür ist die Modallogik T, die Reflexivität definiert und K um das Axiom []a → a erweitert.

Art der Arbeit: Bachelor- oder Masterarbeit

Ansprechpartner: Lutz Schröder


Coalgebraic mu-Calculus

Der klassische mu-Kalkül ist ein Formalismus u.a. zur Beschreibung nebenläufiger Systeme. Seine koalgebraische Variante (siehe z.B. hier) deckt in uniformer Weise verschiedene interessante Erweiterungen ab, wie z.B. den alternierenden mu-Kalkül (zur Beschreibung von Agentensystemen) oder den gradierten mu-Kalkül (mit Zähloperatoren, etwa zur Messung von Redundanz). Als theoretische Arbeiten in diesem Gebiet bieten sich die Entwicklung von Modellprüfungsalgorithen (model checker) oder eine Kodierung von Nominalen, also Namen für einzelne Zustände, an.

Art der Arbeit: Bachelor- oder Masterarbeit

Ansprechpartner: Lutz Schröder


Dr. Tadeusz Litak's proposals


Formalizing LOOP/WHILE languages in Coq

As a part of his BSc project and for teaching purposes of our Chair, Michael Gebhard provided recently an implementation of LOOP/WHILE language as described e.g. in Hoffmann's Theoretische Informatik book. In fact, at our request, the implementation extended the standard setup closer to an ordinary imperative programming language, with global and local variables and full-blown subroutines. However, in order to ensure that LOOP captures exactly primitive recursion and nothing else, the implemented language prevents recursive calls between subroutines.

The goal of the project is thus to formalize syntax and semantics of the LOOP language (and possibly of its WHILE counterpart) and show that it captures exactly the class of primitive recursive functions (recursive functions, respectively).

Another spin-off or fork of the project would be to provide a web-based tool. At present, there is console mode and IntelliJ plugin only.

Art der Arbeit: Any, depending on chosen subproject and the level of difficulty

Ansprechpartner: Tadeusz Litak


Formalizing CTL with fairness

There are several possible ways of extending CTL with fairness constraints, as discussed in the model checking part of the Formal Methods lecture. The goal is to formalize their syntax and semantics in Coq, and formalize some proofs about expressivity of such constraints in the recent extension proposed by Ghilardi and van Gool.

Art der Arbeit: Bachelor oder Master

Ansprechpartner: Tadeusz Litak


Developing metatheory and proof support of GQM and SOPML

This project should be of interest for students, who are interested in the challenge of dealing with syntax with binders in a proof assistant (and semantics of such languages, of course). The formalization in question has been, in fact, quite thoroughly developed by Michael Sammler, capturing our recent paper almost in its entirety. The formalization of the remaining bit, however, is an interesting challenge: it involves the second-order propositional modal logic (SOPML) and some additional semantic notions. Depending on the level of the student, the project can be carried further: it can even involve new results in the form of, e.g., development of Gentzen-style systems for GQM and proving meta-theoretic results about them. The natural further development would be then to create an analogue of Iris/MoSeL interactive Coq proof mode for GQM based on such a system.

Art der Arbeit: Any, depending on chosen subproject and the level of difficulty

Ansprechpartner: Tadeusz Litak


Developing metatheory and proof support of constructive modal logics

This project is a close relative of the preceding one. Apart from Michael Sammler's GQM formalization above, which deals with a formalism based on the classical propositional calculus, another Coq formalization developed previously in our group has dealt with modal logics with intuitionistic propositional base, leading to a FSCD 2017 paper about modal negative translations. There is much more to be done on this front, including formalization of results about formalisms based on Lewis's arrow rather than unary box, their possibly non-Kripkean semantics, fixed-point results and algorithms (some known for a long time in the literature, other currently developed in a collaboration with prof. Alber Visser in Utrecht), their proof systems, possibly with proof-term assignment (i.e., various variants of modal lambda calculi) and their Curry-Howard interpretation in functional programming.

All these themes can be also pursued as theoretical projects for more mathematically inclined students.

Art der Arbeit: Any, depending on chosen subproject and the level of difficulty

Ansprechpartner: Tadeusz Litak


Formalizing Relational Lattices In Coq

Relational lattices provide an algebraic framework for database theory suggested first by Vadim Tropashko from Oracle. While the inventor of relational lattices produced a dedicated tool, the option of formalizing their metatheory in a generic theorem prover like Coq, Agda or Isabelle using the insights of our paper remains both viable and tempting: there are still too many open questions that may be hard to attack otherwise. This project could be enjoyable to veterans of SemProg and/or those of LGruDat. There is also a connection to the next project below: some of our proofs are only available in Prover9, and redoing them in Coq should be an instructive case study.

Art der Arbeit: This would be more suitable for Master students, but given the quality of some BSc students I've seen here, an ambitious Bachelorarbeit is not out of question.

Ansprechpartner: Tadeusz Litak


From Prover9 to Modern Proof Assistants

Prover9 is a rather useful automatic theorem prover whose developer sadly perished in 2009 and since then its development has been frozen. It is rather powerful and still used occasionally (also by me), but apart from the obvious issue of bugs not being fixed and code being increasingly out of date, its output is not particularly readable. A big challenge (which may take more than work of one student…) would be to find an automatic way of translating at least a subclass of proofs generated by Prover9 to proof scripts that can be verified by Isabelle or Coq, thus saving them from the fate of legacy code. One such example and a promising case study is provided by Prover9 library of proofs for relational lattices (see the project above).

Art der Arbeit: This would be more suitable for Master students, but given the quality of some BSc students I've seen here, an ambitious Bachelorarbeit is not out of question.

Ansprechpartner: Tadeusz Litak


Generalizing Classical Model Theory for CPL

This is a project for students who would enjoy a bit more of old fashioned pen-and-paper work, especially rudiments of model theory which appeared in Logische Grundlagen der Datenbanktheorie. In a series of papers (ICALP 2012, TbiLLC 2011, JLC 2017 and LMCS 2018) we have proposed Coalgebraic Predicate Logic (CPL): a generic and natural first-order language to reason about such diverse structures as neighbourhood frames, discrete Markov chains, conditional frames, multigraphs and indeed any type of structure that can be understood in terms of Set-coalgebras. Some basic model theoretical results have been proved for this language, but redoing standard, relational model theory in this much broader setting remains a large task to be completed. It would also generalize a lot of work on topological model theory done by several research centers in Germany in 1970's or 1980's. Some examples of nice, relatively easy warm-up questions have been already suggested in the ICALP paper: obtaining Hilbert-style completeness for some non-compact (but omega-bounded) structures using an omega-rule or investigate a generalization of the omitting types theorem. More challenging ones would include: Beth definability or interpolation, a Keisler-Shelah characterization theorem or a Herbrand theorem.

Art der Arbeit: Any, depending on chosen subproject and the level of difficulty

Ansprechpartner: Tadeusz Litak


Dr. Tadeusz Litak In Kooperation mit Technische Hochschule Nürnberg


This group of projects focuses on further development of VeriGHC: a (Coq-)verified back-end for The Glorious Glasgow Haskell Compilation System, created and maintained by prof. Peter Trommler, a collaborator of our group.

More specifically, the overall project focuses on verifying the last step in the compilation pipeline, i.e., transformation from Cmm to assembly language, in our case PowerPC assembly language, as prof. Trommler wrote most of the PowerPC GHC backend. Cmm is a low-level imperative language, in itself intermediate between C and assembly: a variant of C--.

The main basis of this development is provided by the CompCert project, which produced a verified C (ISO C99) compiler, generating efficient code for the PowerPC, ARM, RISC-V and x86 processors. Our project, however, removes several intermediate steps, following the actual GHC compilation pipeline. Another source of inspiration is DeepSpec, in particular its Haskell component developed by Stephanie Weirich; that development, however, compiled Haskell Core to LLVM rather than the assembly language of a specific processor.


Verified automated Haskell-to-Coq translation

So far, all the Haskell code used in the VeriGHC project has been manually transformed into its AST Coq representation. Recent years, however, have seen increased interest in automating such transformations, a salient example being a 2018 CPP paper, Total Haskell is reasonable Coq. That work has produced the hs-to-coq tool, which was used to verify the Haskell containers library.

Thus, the purpose is to translate the Haskell backend code to Coq and verify its correctness with respect to operational semantics as described in Peter's recent Oberseminar presentation. In order to keep the entire development under control, we are most likely going to exclude calling conventions; see the next project.

Art der Arbeit: Any, depending on chosen subproject and the level of difficulty

Ansprechpartner: Tadeusz Litak


Formalizing calling conventions

This project complements the preceding one. The ELF Application Binary Interface Supplement describes, in particular, function calling sequences of C, whereas for Haskell's Cmm this job seems to be done directly in the code, without a formal specification (apart perhaps from substantial inlined comments). Therefore, our goal is to formalize the calling sequences and prove that the operational semantics of calls matches the operational semantics of Cmm. A further development would be to verify correctness of foreign calls (that is, C calls) in Cmm, building on CompCert and its separation logic.

Art der Arbeit: Any, depending on chosen subproject and the level of difficulty

Ansprechpartner: Tadeusz Litak


Formalizing POWER ISA specification language

This is somewhat orthogonal to the main development of VeriGHC. The Power Instruction Set Architecture (ISA) is a specification that describes the architecture used for IBM POWER processors. It is written following industrial rather than scientific standards, hence its semantics is given in an informal way. Thus, the goal is to formalize it in Coq and prove that the (partial) formalization of PowerPC assembly as provided in CompCert agrees with the POWER ISA specification.

Art der Arbeit: Any, depending on chosen subproject and the level of difficulty

Ansprechpartner: Tadeusz Litak


Coinductive big-step semantics for diverging Cmm programs

The operational semantics of Cmm as presently formalized in VeriGHC is small-step, essentially providing an abstract machine. Nevertheless, as discussed, e.g., in the introduction of this paper, there are still occasions when big-step semantics proves useful, in particular in soundness and completeness proofs. An important limitation of big-step semantics, as you learn in SemProg, is that in its standard incarnation it doesn't allow reasoning about non-terminating programs. To overcome this, Leroy in his development of Cminor provided as an alternative coinductive big-semantics (incomplete, as it doesn't support goto). A brave soul can thus try to provide an analogous development for Cmm.

Art der Arbeit: Theoretically any, though it's hard to imagine this being done below master level

Ansprechpartner: Tadeusz Litak


Rebasing from VST to Iris

At present, the development of VeriGHC is done in the framework of VST by Appel et al. However, in principle nothing would prevent using another major, European framework of the Iris project (currently used, e.g., in the RustBelt project. In general, the degree of portability between these two projects is an important challenge for the community, which has not been fully clarified yet. VeriGHC may provide an important case study.

Art der Arbeit: Theoretically any, though it's hard to imagine this being done below master level

Ansprechpartner: Tadeusz Litak