Themen für Studentische Arbeiten

Model checking is the task of determining whether a reactive system meets a given formal specification, typically expressed in a form of temporal logic. Systems may either be explicitly, by enumerating all system sttates, or in a more compact symbolic representation. The aim of the thesis is to transform existing generic model checking algorithms for coalgebraic fixpoint logics into a symbolic variant.

Many modal and description logic reasoners rely on the tableau methor, which essentially attempts to construct countermodels from syntactic material. The aim of the thesis is to implement the actual extraction of models from runs of a tableau procedure within the Coalgebraic Ontology Logic Solver COOL, a versatile reasoner for a wide variety of logics.

Finite automata have been widely used in computer science and engineering for decades as a powerful tool for modeling and analyzing a wide range of systems and processes. There are various types of automata, such as the classical non-deterministic finite automata (NFA), which works with sets, or the non-deterministic orbit-finite automata (NOFA), which work with nominal sets. These types of automata can be uniformly captured by a notion of automaton in a category, more precisely, a topos.

The language semantics for automata in a topos is straightforward. Since these automata are coalgebras they also have an ensuing coalgebraic semantics. The question is whether this coincides with the language semantics. To answer this question affirmatively one should use the internal language of toposes. In addition (or alternatively) a more direct diagrammatic proof should be possible, and it could be compared with the topos theoretic one. This topic will require a good working knowledge in category theory and the theory of coalgebras. Prior knowledge in topos theory as well as their internal logic would be rather helpful but is not strictly required.

Art der Arbeit: Masterprojekt (ambitioniert) oder Masterarbeit

Ansprechpartner: Stefan Milius

In probabilistischen Beschreibungs- und Modallogiken werden Constraints auf die Wahrscheinlichkeiten für Eigenschaften zufälliger Nachfolger formalisiert, iwie etwa in “der aktuelle Zustand gerärt mit Wahrscheinlichkeit hächstens 5% in einen Deadlock”. Solche Logiken sollen als Instanz in den am Lehrstuhl in Kooperation mit der Australian National University entwickelten generischen Bescheibungslogikreasoner COOL (Coalgebraic Ontology Logic Solver) eingebunden werden.

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 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

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

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

There are several possible ways of extending CTL with fairness constraints, as discussed in the model checking part of the Formal Methods lecture. There are at least two conceivable projects on this subject:

1. The goal of the first one 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 (CTL^f).
2. The goal of the second one is to complexity of compare model checking of CTL^f, including bounded model checking, with that of modern algorithms for well-behaved subclasses of modal fixpoint formulas, many of which are able to express CTL^f formulas. There are powerful modern tools based on such algorithms. The PG Solver overview is a good starting point.

Art der Arbeit: Bachelor oder Master

Ansprechpartner: Tadeusz Litak

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

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

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

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

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

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.

Ansprechpartner: Tadeusz Litak in Kooperation mit TH Nürnberg

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 in Kooperation mti TH Nürnberg

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

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 in Kooperation mit TH Nürnberg

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 in Kooperation mit TH Nürnberg