Software Architectures & Design Calculi

Research team @ HASLab, Univ. Minho

Arca Foundations

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:

Software Components
Lead by Renato Neves, Arca investigates component models and calculi that abstract different computational paradigms. These abstractions include partiality, non-determinism, fuzziness, probabilistic evolution, continuity, quantum, and biology.
Software Architectures
Lead by José Proença, Arca analyses and formalises how heterogeneous and concurrent components interact, inspired by the Reo coordination language. The investigated models and calculi for coordination address notions such as variability and reconfigurability.
Lead by Alexandre Madeira, Arca studies how to use logics, in particular modal logics, to specify and verify properties of computational systems, both at the component and the architecture level. This study is generic and later adapted to specific paradigms and application areas.



Research Associates

Former members

Key Publications since 2015


  • - The frontend for a running server, based on Scala and JavaScript compilation, to bring most tools below developed by Arca members to an interactive and visual web-browser.
  • ReoLive - A web-based project, converting the analysis and visualization of Preo connectors into JavaScript+HTML code.
  • IFTA: Interface Featured Timed Automata - Scala implementation of the Interface Featured Timed Automata (IFTA), including a scala DSL, a composition operator of IFTAs, and an export into UPPAAL Timed Automata with features.
  • Lince - Analysis of hybrid programs using simulation and estimation of approximation errors caused by small perturbations.
  • Preo - parameterised Reo connectors - A clean fork of "parameterised connectors" with emphasis on the language-related aspects.
  • Parameterised connectors - A language for type-checking families of connectors.
  • PICC: Partial Interactive Coordination Constraints - A constraint-based engine in Scala for running connectors based on Reo.

Check our GitHub site at


List of contributions to other projects.
  • Hets - Added support for HybridCASL, providing a method to automatically combine the standard properties of hybrid logics with any logic already integrated in Hets.


  • DaVinci


    Distributed Architectures: Variability and Interaction for Cyber-Physical Systems; Started in 2018.

  • KLEE


    Coalgebraic Modeling and Analysis for Computational Synthetic Biology; Started in 2018.

  • DaLí


    Dynamic logics for cyber-physical systems; 2016–2018.


We are also involved in the following projects.
  • LightKone


    Lightweight computation for networks at the edge; 2017–2020.



    Trustworthy Software Design with Alloy; 2016–2018.

  • SmartEGOV

    (P2020 NORTE-45-2015-23) Harnessing EGOV for smart governance: Foundations and tools, since May, 2016.

Ongoing PhD and Master projects

  • [PhD] Quantum algebraic specifications, by Carlos Tavares.

    Supervisor: Luís Barbosa.

    This project investigates algebraic approaches to specify and analyse quantum computer science.

  • [PhD] Dynamising dynamic logic, by Leandro Gomes.

    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.

Past Projects

  • [Master] Animation of monad H, by Tiago Loureiro.

    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.

  • [PhD] Logics and calculi for cyber–physical components, by Renato Neves.

    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.

  • [PhD] A Virtual Factory for Smart City Service Integration, by Guillermina Cledou.

    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.


  • Cyber-Physical Computation (2019/20) For PhD students, on fundamental concepts and formal methods to analyse cyber-physical systems, assuming time evolves continuously.
  • Quantum Computing (MAP-i) (2020/21, 2019/20) For PhD students, on fundamental concepts and formal methods in Quantum Computing.
  • Software architecture and Calculi (2020/21, 2019/20, 2018/19, 2017/18, 2016/17, 2015/16) For Master students, on how to model and analyse concurrent systems.
  • Interaction and Concurrency (2020/21, 2019/20, 2018/19, 2017/18, 2016/17) 3rd year course on process algebra and other concurrency models.
  • Algebraic and Coalgebraic Models in Software Development (2016/17) For PhD students - Doctoral program of MAP-i, including the universities of Minho, Aveiro and Porto.
  • Quantum Logic (2020/21, 2019/20, 2018/19, 2017/18)
  • Quantum Computing (2021/22, 2020/21, 2019/20, 2018/19, 2017/18, 2016/17)
  • Mathematics for Computer Science (2017/18) An introductory course to Logic and Relations given to external students.

Research Opportunities

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.

Alloy and Hybrid Logic

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

Model checking R/G programs in Alloy

(Funded by the Trust project.)

When you run a program on your lap-top you "rely" on the operating system not letting any other program to interfere with your state space. But programs could be designed in a collaborative-style, with sub-programs helping each other over a shared state. (Example: on-the-fly garbage collection.) In the early 1980s, Cliff Jones proposed a dynamic extension to (static) Hoare logic: further to pre / post conditions, one could also specify interference of the environment via rely / guarantee conditions. Interest on R/G programming is growing a lot due to its potential for concurrency.

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.

From specifications to concrete processes

(Funded by the DaLí project.)

This project aims at studying a dynamic logic with binders, and (automatic) translations from specifications in (some fragment) of this logic into a concrete process algebra.

Quantum Programming Languages

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

[PhD] Making Logics Coalgebraic

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

Dissemination events

Arca Meetings

We meet every two weeks to discuss ongoing work within the team.

Upcoming meetings

Previous meetings