Cookies Policy
The website need some cookies and similar means to function. If you permit us, we will use those means to collect data on your visits for aggregated statistics to improve our service. Find out More
Accept Reject
  • Menu
Presentation

High-Assurance Software

At the High-Assurance Software Laboratory (HASLab), we improve practice through theory, creating and implementing software that goes beyond mere functionality: we ensure it is correct, resilient, and secure against failures and attacks.


Our team of researchers, scientists, and engineers has proven expertise in software engineering, developing methods and tools to design and integrate robust software; in distributed systems, exploring distribution and replication to ensure scalability and reliability; and in information security, addressing cybersecurity challenges and improving systems with advanced, secure cryptographic protocols, thus minimising vulnerabilities.


With a multidisciplinary approach supported by solid theoretical principles, we develop innovative solutions for critical software, secure cloud infrastructures, and privacy-aware big data management, driving scientific advancement, innovation, and high-level consultancy.


In addition, we complement our core expertise with work in human-computer interaction, programming languages, computational mathematics, and quantum computing - because we believe the future of trustworthy software is built on knowledge and innovation.

Interest
Topics
081

Featured Projects

POISE

Programmable Asynchronous Asymmetric Secure Choreographies

2026-2027

QUANTHOS

QUANTHOS - Fotónica Integrada Topológica Quântica

2026-2027

Rescueware

Cibersegurança e Recuperação de Dados Inteligente e Auto-Configurável para a Resiliência contra Ransomware

2026-2029

HPCTRAIN

EuroHPC traineeships in Hosting Entities, Centres of Excellence and Competence Centres, SMEs and Industry

2026-2029

ADAPQO

Adaptive Query Optimization Architectures to Support Heterogeneous Data Intensive Applications

2025-2026

QuantumCLP

Quantum computing optimization for container loading problems: a new frontier in logistics optimization

2025-2027

BANSKY

A paraconsistent inference engine to support research in age-ralated molecular degeneration

2025-2028

JasminCode

Developing Reliable High-performance Assembly Code using Jasmin

2025-2026

TestBed5G_Robotics

Piloto de Robótica Móvel e Cibersegurança em Ambientes Industriais sobre Comunicações 5G – Europneumaq

2025-2026

ATAI

Aplicação de técnicas avançadas na gestão de escalas

2025-2027

BringTrust

Strengthening CI/CD Pipeline Cybersecurity and Safeguarding the Intellectual Property

2025-2028

SafeIaC

SafeIaC: Reliable Analysis and Automated Repair for Infrastructure as Code

2025-2028

PFAI4_6eD

Programa de Formação Avançada Industria 4 - 6a edição

2025-2025

INSIEME

Integrated Network for data Space and Interoperable Energy Management in Europe

2025-2028

DisaggregatedHPC

Towards energy-efficient, software-managed resource disaggregation in HPC infrastructures

2025-2026

InfraGov

InfraGov: A Public Framework for Reliable and Secure IT Infrastructure

2025-2026

VeriFixer

VeriFixer: Automated Repair for Verification-Aware Programming Languages

2025-2026

JRCSIF

JRC Interoperability Laboratory Adoption of the Semantic Interoperability Framework

2025-2025

CDMS

Claim Denial Management Solution

2025-2026

BolsasFCT_Gestao

Funding FCT PhD Grants - Management

2025-9999

ENSCOMP4

Ensino de Ciência da Computação nas Escolas 4

2024-2026

PeT

PeT - Privacidade e Transparência

2024-2028

PFAI4_5eD

Programa de Formação Avançada Industria 4 - 5a edição

2024-2024

exaSIMPLE

exaSIMPLE: A Hybrid ML-CFD SIMPLE Algorithm for the Exascale Era

2024-2025

EPICURE

High-level specialised application support service in High-Performance Computing (HPC)

2024-2028

BCDSM

BCD.S+M - Modular Blockchain Data Storage and Management System with AI

2024-2027

TwinEU

Digital Twin for Europe

2024-2026

HEDGE_IoT

Holistic Approach towards Empowerment of the DiGitalization of the Energy Ecosystem through adoption of IoT solutions

2024-2027

HANAMI

Hpc AlliaNce for Applications and supercoMputing Innovation: the Europe - Japan collaboration

2024-2027

PFAI4_4eD

Programa de Formação Avançada Industria 4 - 4a edição

2023-2023

QuantELM

QuantELM: from Ultrafast optical processors to Quantum Extreme Learning Machines with integrated optics

2023-2024

ATE

Alliance for Energy Transition

2023-2026

Green_Dat_AI

Energy-efficient AI-ready Data Spaces

2023-2025

EuroCC2

National Competence Centres in the framework of EuroHPC Phase 2

2023-2026

AURORA

Deteção de atividade no interior do veículo

2022-2023

ATTRACT_DIH

Digital Innovation Hub for Artificial Intelligence and High-Performance Computing

2022-2026

NewSpacePortugal

Agenda New Space Portugal

2022-2026

BeFlexible

Boosting engagement to increase flexibility

2022-2026

ENERSHARE

European commoN EneRgy dataSpace framework enabling data sHaring-driven Across- and beyond- eneRgy sErvices

2022-2025

Gridsoft

Parecer sobre a implementação de software para redes elétricas inteligentes

2022-2022

PFAI4_3ed

Programa de Formação Avançada Industria 4 - 3a edição

2022-2022

THEIA

Automated Perception Driving

2022-2023

IBEX

Métodos quantitativos para a programação ciber-física: Uma abordagem precisa para racicionar sobre imprecisões na computação ciber-física

2022-2025

SpecRep

Constraint-based Specification Repair

2022-2023

FLEXCOMM

Towards Energy-aware Communications: Connecting the power grid and communication infrastructure

2022-2023

IDINA

Identidade Digital Inclusiva Não Autoritativa

2021-2025

Sustainable HPC

Computação de elevado desempenho sustentável

2021-2025

CircThread

Building the Digital Thread for Circular Economy Product, Resource & Service Management

2021-2025

PassCert

Exploring the Impact of Formal Verification on the Adoption of Password Security Software

2021-2022

IoT4Distribuicao

Análise de Requisitos e Especificação Funcional de uma Arquitetura Distribuída baseada em soluções IoT para a Gestão e Controlo da Rede de Distribuição

2021-2023

RISC2

A network for supporting the coordination of High-Performance Computing research between Europe and Latin America

2021-2023

DigiLightRail

Solução de Automação do Ciclo de Vida de Projectos de Sinalização Ferroviária

2020-2023

PFAI4.0

Programa de Formação Avançada Industria 4.0

2020-2021

PAStor

Programmable and Adaptable Storage for AI-oriented HPC Ecosystems

2020-2021

ACTPM

Automating Crash-Consistency Testing for Persistent Memory

2020-2021

AIDA

Adaptive, Intelligent and Distributed Assurance Platform

2020-2023

BigHPC

A Management Framework for Consolidated Big Data and HPC

2020-2023

SLSNA

Prestação de Serviços no ambito do projeto SKORR

2020-2021

InterConnect

Interoperable Solutions Connecting Smart Homes, Buildings and Grids

2019-2024

T4CDTKC

Training 4 Cotec, Digital Transformation Knowledge Challenge - Elaboração de Programa de Formação “CONHECER E COMPREENDER O DESAFIO DAS TECNOLOGIAS DE TRANSFORMAÇÃO DIGITAL”

2019-2021

CLOUD4CANDY

Cloud for CANDY

2019-2019

HADES

HArdware-backed trusted and scalable DEcentralized Systems

2018-2022

MaLPIS

Aprendizagem Automática para Deteção de Ataques e Identificação de Perfis Segurança na Internet

2018-2022

SKORR

Advancing the Frontier of Social Media Management Tools

2018-2021

DaVinci

Distributed architectures: variability and interaction for cyber-physical systems

2018-2022

SAFER

Safery verification for robotic software

2018-2021

KLEE

Coalgebraic modeling and analysis for computational synthetic biology

2018-2021

InteGrid

Demonstration of INTElligent grid technologies for renewables INTEgration and INTEractive consumer participation enabling INTEroperable market solutions and INTErconnected stakeholders

2017-2020

Lightkone

Lightweight Computation for Networks at the Edge

2017-2019

CloudDBAppliance

European Cloud In-Memory Database Appliance with Predictable Performance for Critical Applications

2016-2019

Cloud-Setup

PLATAFORMA DE PREPARAÇÃO DE CONTEÚDOS AUDIOVISUAIS PARA INGEST NA CLOUD

2016-2019

GSL

GreenSoftwareLab: Towards an Engineering Discipline for Green Software

2016-2019

CORAL-TOOLS

CORAL – Sustainable Ocean Exploitation: Tools and Sensors

2016-2018

SafeCloud

Secure and Resilient Cloud Architecture

2015-2018

NanoStima-RL1

NanoSTIMA - Macro-to-Nano Human Sensing Technologies

2015-2019

NanoStima-RL3

NanoSTIMA - Health data infrastructure

2015-2019

SMILES

SMILES - Smart, Mobile, Intelligent and Large scale Sensing and analytics

2015-2019

UPGRID

Real proven solutions to enable active demand and distributed generation flexible integration, through a fully controllable LOW Voltage and medium voltage distribution grid

2015-2017

LeanBigData

Ultra-Scalable and Ultra-Efficient Integrated and Visual Big Data Analytics

2014-2017

Practice

Privacy-Preserving Computation in the Cloud

2013-2016

CoherentPaaS

A Coherent and Rich PaaS with a Common Programming Model

2013-2016

Team
  • a
  • b
  • c
  • d
  • e
  • f
  • g
  • h
  • i
  • j
  • k
  • l
  • m
  • n
  • o
  • p
  • q
  • r
  • s
  • t
  • u
  • v
  • w
  • x
  • y
  • z
Publications

HASLab Publications

View all Publications

2021

Towards a bottom-up approach to inclusive digital identity systems

Authors
Silva, JMC; Fonte, V; Sousa, A;

Publication
ICEGOV 2021: 14th International Conference on Theory and Practice of Electronic Governance, Athens, Greece, October 6 - 8, 2021

Abstract

2021

Hubs for VirtuosoNext: Online verification of real-time coordinators

Authors
Cledou, G; Proença, J; Sputh, BHC; Verhulst, E;

Publication
SCIENCE OF COMPUTER PROGRAMMING

Abstract
VirtuosoNextTM is a distributed real-time operating system (RTOS) featuring a generic programming model dubbed Interacting Entities. This paper focuses on these interactions, implemented as so-called Hubs. Hubs act as synchronisation and communication mechanisms between the application tasks and implement the services provided by the kernel. While the kernel provides the most basic services, each carefully designed, tested and optimised, tasks are limited to this handful of basic hubs, leaving the development of more complex mechanisms up to application specific implementations. This work presents a toolset that supports the building of new services compositionally, using notions borrowed from the Reo coordination language, on which the developer can delegate coordination-related duties. This toolset uses a formal compositional semantics for hubs that captures dataflow and time, formalising the behaviour of existing hubs, and allowing the definition of new ones. Furthermore, it enables the analysis and verification of hubs under our automata interpretation, including time-sensitive behaviour via the UPPAAL model checker, usable on http://arcatools .org /hubs. We illustrate the proposed tools and methods by verifying key properties on different interaction scenarios between tasks and a composed hub.

2021

Featured Team Automata

Authors
ter Beek, MH; Cledou, G; Hennicker, R; Proenca, J;

Publication
FORMAL METHODS, FM 2021

Abstract
We propose featured team automata to support variability in the development and analysis of teams, which are systems of reactive components that communicate according to specified synchronisation types. A featured team automaton concisely describes a family of concrete product models for specific configurations determined by feature selection. We focus on the analysis of communication-safety properties, but doing so product-wise quickly becomes impractical. Therefore, we investigate how to lift notions of receptiveness (no message loss) to the level of family models. We show that featured (weak) receptiveness of featured team automata characterises (weak) receptiveness for all product instantiations. A prototypical tool supports the developed theory.

2021

A Proposal for the Classification of Methods for Verification and Validation of Safety, Cybersecurity, and Privacy of Automated Systems

Authors
la Vara, JLd; Bauer, T; Fischer, B; Karaca, M; Madeira, H; Matschnig, M; Mazzini, S; Nandi, GS; Patrone, F; Pereira, D; Proença, J; Schlick, R; Tonetta, S; Yayan, U; Sangchoolie, B;

Publication
QUATIC

Abstract
As our dependence on automated systems grows, so does the need for guaranteeing their safety, cybersecurity, and privacy (SCP). Dedicated methods for verification and validation (V&V) must be used to this end and it is necessary that the methods and their characteristics can be clearly differentiated. This can be achieved via method classifications. However, we have experienced that existing classifications are not suitable to categorise V&V methods for SCP of automated systems. They do not pay enough attention to the distinguishing characteristics of this system type and of these quality concerns. As a solution, we present a new classification developed in the scope of a large-scale industry-academia project. The classification considers both the method type, e.g., testing, and the concern addressed, e.g., safety. Over 70 people have successfully used the classification on 53 methods. We argue that the classification is a more suitable means to categorise V&V methods for SCP of automated systems and that it can help other researchers and practitioners.

2021

The VALU3S ECSEL project: Verification and validation of automated systems safety and security

Authors
Agirre, JA; Etxeberria, L; Barbosa, R; Basagiannis, S; Giantamidis, G; Bauer, T; Ferrari, E; Esnaola, ML; Orani, V; Öberg, J; Pereira, D; Proença, J; Schlick, R; Smrcka, A; Tiberti, W; Tonetta, S; Bozzano, M; Yazici, A; Sangchoolie, B;

Publication
Microprocess. Microsystems

Abstract
Manufacturers of automated systems and their components have been allocating an enormous amount of time and effort in R&D activities, which led to the availability of prototypes demonstrating new capabilities as well as the introduction of such systems to the market within different domains. Manufacturers need to make sure that the systems function in the intended way and according to specifications. This is not a trivial task as system complexity rises dramatically the more integrated and interconnected these systems become with the addition of automated functionality and features to them. This effort translates into an overhead on the V&V (verification and validation) process making it time-consuming and costly. In this paper, we present VALU3S, an ECSEL JU (joint undertaking) project that aims to evaluate the state-of-the-art V&V methods and tools, and design a multi-domain framework to create a clear structure around the components and elements needed to conduct the V&V process. The main expected benefit of the framework is to reduce time and cost needed to verify and validate automated systems with respect to safety, cyber-security, and privacy requirements. This is done through identification and classification of evaluation methods, tools, environments and concepts for V&V of automated systems with respect to the mentioned requirements. VALU3S will provide guidelines to the V&V community including engineers and researchers on how the V&V of automated systems could be improved considering the cost, time and effort of conducting V&V processes. To this end, VALU3S brings together a consortium with partners from 10 different countries, amounting to a mix of 25 industrial partners, 6 leading research institutes, and 10 universities to reach the project goal.