1st Semester 2010/11: From Category Theory to Implementation: A Behavioural Symmetry-Reduction Algorithm

Instructors

Vincenzo Ciancia
If you are interested in this project, please contact Vincenzo by email.

ECTS

6

Description

One of the most well-known applications of logic in computer science is model-checking, which consists in an exhaustive search of the state space of a (typically concurrent) system to verify certain properties. The problem is inherently exponential in the size of a program. Among the many techniques to reduce the state space, E .A. Emerson -- who received the Turing award in 2007 for pionieering model checking -- proposed and studied in detail the use of the implicit symmetry of a program, e.g., commutativity of parallel composition. In his approach, it is up to the user to input a description of the symmetry, that is, the operations that "leave the program unchanged" under some notion of semantics.

However, real programs tend to be complex, and there is hidden symmetry that is not visible at the syntactic level, but only in the semantics of a program. This makes the above approach sub-optimal, as only some of the possible state-space reductions will be effectively used.

In joint work with Alexander Kurz and Ugo Montanari, I developed a simple automatic procedure to compute the symmetry of a system, by looking at its semantics instead of its syntax. The technique relies on final coalgebra semantics in a presheaf category. The algorithm takes as an input a state of a system, and returns the greatest group of operations under which the semantics of the program remains unchanged.

The goal of the project is to write a reference implementation of the algorithm in a functional programming language. This requires some background in coalgebras and of course some functional programming skills. The size of the implementation is expected to be very small (in the order of some hundreds of lines of code).

The main interest in doing such a project is learning how a very abstract mathematical framework can be used to define a "correct by construction" implementation. The project may evolve into a research paper.