Cohesive Project (Lab. EI)


Interesting and useful slides for preparing your milestone presentations:


Group Project Partnership External supervisor(s) Tutors Nr Student Photo
G1 CLAV - Public Information Classification and Evaluation: formal model specification Algoritmi J.C. Ramalho J.N. Oliveira a77628 Armando Santos a77628
a77508 Gonçalo Duarte a77508
G2 Analysis of connectors in Alloy HASLab J.M. Proença N.M. Macedo a78912 Miguel Pereira a78912
a78434 Pedro Silva  a78434
G3 Alloy for ASML machine sequence generation ASML (NL) André Santos J.N. Oliveira a79021 Diogo Silva a79021
a78961 Tiago Monteiro a78961
G4 Studying Automatic Differentiation CMAT Pedro Patrício J.N. Oliveira pg38014 Artur Queiroz pg38014
pg38413 Ezequiel Moreira pg38413
pg37020 Nelson Loureiro pg37020


1st Checkpoint - March the 27th

2nd Checkpoint -


Final evaluation by industrial partners: our Skype-ID: uminho-di-a1

Project descriptions

Project 1 - CLAV - Public Information Classification and Evaluation: formal model specification (J.C. Ramalho)

  • CLAV is a platform being developed by DI/UM with the partnership and ordered by the Direção Geral do Livro, Arquivos e Bibliotecas (DGLAB) which aims the classification and evaluation of all documents that move around and across portuguese public institutions. One view, already visible, of the project is the so called Lista Consolidada, which is a comprehensive catalog of all administrative processes ocurring in Portuguese public institutions. The first version is available online. For further information contact the author. There are several articles and presentations about this subject. Currently, the model is specified in OWL ("Ontology Web Language"), but suffered several changes during the last year and there was no time to study the impact of those changes in the model's pre-conditions and invariants. In this project we want: (a) to formally specify the model from scratch; (b) to load the available information onto the new model; (c) to specify pre-conditions and invariants; (d) to report errors.

Project 2 - Relational algebra for data processing using strongly typed FP (J.P. Magalhães, Standard Chartered Bank, Singapore)

  • Relational algebra is a powerful and versatile tool for data processing. Previous work on adding static types to a relational algebra library has turned "reasoning and proving properties of programs" into simply "typechecking". However, we are often concerned about more than just the type of a relation; we might care about the keys, or the size of the relation, for example. A common use case is to process a large relation until it contains a single row with the desired answer, but currently we cannot statically express the constraint that the relation has a single row. This project looks at extending Augustsson and Ågren's earlier work to deal with such constraints (and possibly others).

Project 3 - Alloy for ASML machine sequence generation (André Passos, ASML, NL)

  • See the following slides: PDF.

Project 4 - Analysis of connectors in Alloy (Nuno Macedo, José Proença)

Reo is a language to specify how software components interact with each other. Reo programs are called connectors - the formal semantics of these are based on transition systems that quickly become huge. The best existing approach to verify properties of such connectors rely on an external model checker based on process algebra, mCRL2, which does not cope well with (infinitely) large state spaces.

Alloy is a high-level specification language with support for automatic model finding. The language, based on relational logic, is simple and flexible, allowing the declarative specification of systems with variable configurations and alternative behaviours. Unlike in mCRL2, an Alloy specification does not explicitly describe the transition system, making it better suited to abstract away certain concepts, such as time, data, or variability.

The key scientific goal is to understand and extend the approach to model connectors with Alloy by Khosrav et al., e.g., introducing notions of time or variability.


The key technical goal is to extend the ReoLive tools with support for Alloy, similar to how it is currently done for mCRL2, which will involve learning basics of Scala and JavaScript.


Project 5 - Studying Automatic Differentiation (Pedro Patrício)

  • This theme is proposed for MMC students. It consists in carefully studying and presenting a recent paper on this topic (The Simple Essence of Automatic Differentiation by C. Elliott, POPL 2019) including some experimentation with the library described there. A second objective is to see how it could be applied in the context of typed neural networks. There is also a video:youtube.