Below are the recently completed student projects within the Fundamental Computing group. Unless stated otherwise, these projects were part of the degree programmes for Computing Science at the University of Groningen.
-
Bounded countermodels for fragments of FLec
Supervised by Dan Frumin, Revantha Ramanayake
-
Formal Verification of Leftist and Skew Heaps in Rocq
Supervised by Dan Frumin, Jorge Perez
-
Formal Verification of Pairing Heaps in Rocq
Supervised by Dan Frumin, Jorge Perez
-
Interplay of Number Theory and Fixed-Parameter Tractable Algorithms
Supervised by Ivan Bliznets
-
Model Structures and Infinity Categories
Supervised by Dan Frumin, Oliver Lorscheid
-
Programming and Reasoning with Monads
Supervised by Dan Frumin, Jorge Perez
-
Verified Functional Graph Algorithms using The Rocq Prover
Supervised by Dan Frumin, Jorge Perez
-
Concurrent Programming Using Multicore OCaml
Supervised by Dan Frumin, Jorge Perez
-
Formal Verification of 2-3 Trees in Coq
Supervised by Dan Frumin, Jorge Perez
-
The Leader Election Problem in a Typed Pi-calculus
Supervised by Jorge Perez, Dan Frumin
-
Automated Proof Search in a Cyclic Proof System for Game Logic
Supervised by Helle Hvid Hansen, Revantha Ramanayake
-
Comparing Deadlock-Free Processes, Revisited
Supervised by Jorge Perez
-
Deduction Proof Evaluator for Fitch Style Proofs
Supervised by Helle Hvid Hansen, Daniel Feitosa
-
A Model Checker for Game Logic via Parity Games
Supervised by Helle Hvid Hansen, Jorge Perez
-
A dynamic approach to protocol conformance verification using multiparty session types
Supervised by Jorge Perez, Bas van den Heuvel
-
Automating XML parser generation for specific data operations
Supervised by Fadi Mohsen, Jorge Perez
-
Enhancing the Automata Theory Course with Notions from Reactive Systems
Supervised by Jorge Perez, Revantha Ramanayake
-
Formalization of modal logic S5 in the Coq proof assistant
Supervised by Dan Frumin, Revantha Ramanayake
-
Game Logic: A Proof Transformation from Gentzen to Hilbert
Supervised by Helle Hvid Hansen, Tijs van der Storm
-
Hoare Logics for Skeletal Semantics
Supervised by Dan Frumin, Jorge Perez
-
Linear algorithms for Parity Games with the Signature of a Potential
Supervised by Oliver Lorscheid, Jorge Perez
-
Skeletal semantics for message-passing concurrency - from actors to channels and back
Supervised by Dan Frumin, Jorge Perez
-
Towards Automated Theorem Proving in the CloG Proof System
Supervised by Helle Hvid Hansen, Revantha Ramanayake
-
Completeness over Kripke models of a cyclic proof system for game logic
Supervised by Helle Hvid Hansen, Alef Sterk
-
Executable Specifications of Message-based Concurrency in Maude
Supervised by Jorge Perez, Dan Frumin
-
From Accepting Computation to Satisfying Kripke Model
Supervised by Helle Hvid Hansen, Revantha Ramanayake
-
Proof Transformations for Game Logic
Supervised by Helle Hvid Hansen, Tijd van der Storm
-
Strong Normalization in Message-Passing Concurrency
Supervised by Jorge Perez