Arca – Software Architecture & Design Calculi – is a research team lead by prof. Luís Barbosa and prof. José Nuno Oliveira. It investigates formal approaches based on calculi of programs, processes, algorithms, etc. and on software quality, focusing on components, architectures, coordination, and variability.
This team is part of the HASLab group, which is a software laboratory the university of Minho associated to INESC TEC.
Arca is articulated to a new research group on Quantum Software Engineering, hosted by INL, the International Iberian Nanotechnology Laboratory, lead by Luis Soares Barbosa.
Arca is grounded on 3 fundamental pilars:
Full Professor at INESC TEC and Univ. Minho.
Full Professor at INESC TEC, Univ. Minho, and QuantaLab.
Assistant professor at CIDMA.
Post-Doc at INESC TEC and Univ. Minho.
Post-Doc at CISTER
Post-Doc at INESC TEC and Univ. Minho.
PhD researcher at INESC TEC and Univ. Minho.
PhD researcher at INESC TEC and Univ. Minho.
PhD researcher at INESC TEC and Univ. Minhom and a UNU-EGOV Fellow at the United Nations University.
Master student at INESC TEC and Univ. Minho.
Master student at Univ. Minho.
Associate professor at Univ. Aveiro.
PhD researcher at Univ. Aveiro.
Check our GitHub site at https://github.com/arcalab.
Distributed Architectures: Variability and Interaction for Cyber-Physical Systems; Will start in 2018.
Coalgebraic Modeling and Analysis for Computational Synthetic Biology; Will start in 2018.
Dynamic logics for cyber-physical systems; 2016–2018.
Lightweight computation for networks at the edge; 2017–2020.
Trustworthy Software Design with Alloy; 2016–2018.
(P2020 NORTE-45-2015-23) Harnessing EGOV for smart governance: Foundations and tools, since May, 2016.
Supervisor: Luís Barbosa.
This project investigates algebraic approaches to specify and analyse quantum computer science.
Supervisor: Luís Barbosa.
This project aims at building a systematic process of generating dynamic logic, by developing a general theory of such logics. This approach favours a contract-based design method for software specification, and the development of an algebraic structure to model the space of programs and the corresponding domains of behaviours.
Supervisors: Luís Barbosa and Renato Neves.
This project proposes an Haskell implementation for hybrid systems, capable of visually depicting the evolution of continuous functions.
Supervisor: Luís Barbosa.
This project focuses mainly on the foundations of cyber physical systems; coalgebras, proof theory and institutional theory. It also covers a myriad of logics, in particular modal logics.
Supervisors: Luís Barbosa and Elsa Estevez.
The aim of the thesis is to advance the state of the art in software modelling and development tools for the rapid development of integrated city-level electronic public services.
These is a selection of possible projects for master students that would like to work with us. We are also open for discussion about other topics. Note that we have a few grants that can pay for most of the ideas presented in these projects. If you are interested, just come and talk to us.
(Funded by either the Trust or the DaLí project.)
The purpose of this project is to explore a variant of hybrid logics in which worlds are equipped with Alloy models. In principle, such a logic (generated via the hybridisation method "hybridisation") provides a canonical language to address reconfigurability in Alloy specifications.
The workplan involves the implementation of a calculus for this logic (reported in Proof theory for hybridised logics) and the development of a case study that illustrates its potentialities (and limitations) in the software development process.
(Funded by the Trust project.)
When you run a program on your lap-top you "
In this project we would like to use Alloy to model the semantics of a simple imperative language with R/G commands and model-check their interference. The idea is to find design errors of (possibly non-terminating) R/G programs by analysing finite traces only.
(Funded by the DaLí project.)
This project aims at studying aThis project aims at exploring the field of quantum programming languages and quantum artificial intelligence in a new line of research of the group of formal methods of Department of Informatics. The project involves the implementation of some quantum algorithms and its comparison with more classical approaches.
(Funded by the DaLí project.)
The main goal of this PhD project is the development of a general notion of asymmetric combination of logic that turns logics coalgebraic. More concretely, a process that equips any given logic with suitable coalgebraic machinery re- spective to a given functor; this means that, in contrast to hybridisation, or temporalisation, the input parameter is not just the base logic, but also the functor that gives rise to the intended type of transitions.
We meet every two weeks to discuss ongoing work within the team.
