Cohesive Project (Lab. EI)

Material

Interesting and useful slides for preparing your milestone presentations:

• http://research.microsoft.com/en-us/um/people/simonpj/papers/giving-a-talk/writing-a-paper-slides.pdf

Projects

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
					a77508	Gonçalo Duarte
G2	Analysis of connectors in Alloy	HASLab	J.M. Proença	N.M. Macedo	a78912	Miguel Pereira
					a78434	Pedro Silva
G3	Alloy for ASML machine sequence generation	ASML (NL)	André Santos	J.N. Oliveira	a79021	Diogo Silva
					a78961	Tiago Monteiro
G4	Studying Automatic Differentiation	CMAT	Pedro Patrício	J.N. Oliveira	pg38014	Artur Queiroz
					pg38413	Ezequiel Moreira
					pg37020	Nelson Loureiro

Milestones

1st Checkpoint - March the 27th

2nd Checkpoint -

Evaluation

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.

* https://pdfs.semanticscholar.org/c1d0/78be0aa0d88baf12501668c32e2dcda8ede1.pdf

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.

* https://reolanguage.github.io/ReoLive/snapshot/

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