Cohesive Project (Lab. EI)
Material
Interesting and useful slides for preparing your milestone presentations:
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 |  |
| G1 | CLAV - Public Information Classification and Evaluation: formal model specification | Algoritmi | J.C. Ramalho | J.N. Oliveira | a77508 | Gonçalo Duarte |  |
| G3 | Alloy for ASML machine sequence generation | ASML (NL) | André Santos | J.N. Oliveira | a79021 | Diogo Silva |  |
| G3 | Alloy for ASML machine sequence generation | ASML (NL) | André Santos | J.N. Oliveira | a78961 | Tiago Monteiro |  |
| G4 | Studying Automatic Differentiation | CMAT | Pedro Patrício | J.N. Oliveira | pg38014 | Artur Queiroz |  |
| G4 | Studying Automatic Differentiation | CMAT | Pedro Patrício | J.N. Oliveira | pg38413 | Ezequiel Moreira |  |
| G4 | Studying Automatic Differentiation | CMAT | Pedro Patrício | J.N. Oliveira | pg37020 | Nelson Loureiro |  |
| G2 | Analysis of connectors in Alloy | HASLab | J.M. Proença | N.M. Macedo | a78912 | Miguel Pereira |  |
| G2 | Analysis of connectors in Alloy | HASLab | J.M. Proença | N.M. Macedo | a78434 | Pedro Silva |  |
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:
.