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.

news
Interest
Topics
085

Featured Projects

INOCULUM

Boosting the Immunity of Storage Systems Against Ransomware

2026-2029

MOBOT2

Manipulador Móvel Inteligente com Programação Intuitiva e Controlo Agnóstico

2026-2029

EuroCC3

National Competence Centres in the framework of EuroHPC Phase 3

2026-2029

QuantumCLP

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

2026-2027

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

QUANTUM_IBER_IA

QUANTUM IBER_IA: Impulso estratégico de las capacidades en tecnologías cuánticas e inteligencia artificial en el espacio ibérico transfronterizo

2026-2028

ADAPQO

Adaptive Query Optimization Architectures to Support Heterogeneous Data Intensive Applications

2025-2026

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-2026

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

2026

Auto-active verification of distributed systems and specification refinements with Why3-do

Authors
Lourenço, CB; Pinto, JS;

Publication
SCIENCE OF COMPUTER PROGRAMMING

Abstract
In this paper, we introduce a novel approach for rigorously verifying safety properties of state machine specifications. Our method leverages an auto-active verifier and centers around the use of action functions annotated with contracts. These contracts facilitate inductive invariant checking, ensuring correctness during system execution. Our approach is further supported by the Why3-do library, which extends the Why3 tool's capabilities to verify concurrent and distributed algorithms using state machines. Two distinctive features of Why3-do are: (i) it supports specification refinement through refinement mappings, enabling hierarchical reasoning about distributed algorithms; and (ii) it can be easily extended to make verifying specific classes of systems more convenient. In particular, the library contains models allowing for message-passing algorithms to be described with programmed handlers, assuming different network semantics. A gallery of examples, all verified with Why3 using SMT solvers as proof tools, is also described in the paper. It contains several auto-actively verified concurrent and distributed algorithms, including the Paxos consensus algorithm.

2026

ConflictSync: Bandwidth Efficient Synchronization of Divergent State

Authors
Baquero, C; Gomes, PS; Rodrigues, MB;

Publication
PaPoC@EuroSys

Abstract
State-based Conflict-Free Replicated Data Types (CRDTs) are widely used in distributed systems to ensure high availability without coordination. However, their naive synchronization strategy, transmitting the full state, incurs high communication costs. In this paper, we: (1) propose ConflictSync, a digest-driven synchronization algorithm, which reduces total data transfer by up to 18× compared to full-state transmissions; (2) formulate state-based CRDT synchronization as set reconciliation over irredundant join decompositions; (3) generalize Rateless Set Reconciliation for variable-sized elements, at the cost of an additional communication step; (4) introduce a new generic set reconciliation solution, integrating Bloom Filters with rateless IBLTs; (5) experimentally evaluate the novel synchronization strategies. © 2026 Copyright held by the owner/author(s).

2026

Bounding Byzantine Impact in Open CRDT Systems

Authors
Baquero, C; Maia, F; Dantas, A; Anta, AF; Frey, D; Sánchez, C; Albouy, T;

Publication
PaPoC@EuroSys

Abstract
Conflict-free Replicated Data Types (CRDTs) enable available and eventually consistent data replication without coordination, making them well suited for open and partition-prone environments. Recent work has shown that CRDTs can be extended to tolerate Byzantine faults by ensuring that replicas eventually agree on the validity of operations, even in permis-sionless settings. However, validity alone does not prevent a Byzantine participant from inflicting unbounded damage by issuing large volumes of adversarial yet well-formed updates. For example, when editing text, an attacker can easily delete prior text. In this paper, we study how to bound the impact of Byzantine behavior in open CRDT systems. We introduce bounded Byzantine CRDTs, a rate-limiting framework for CRDTs in which each update carries an associated cost that limits the influence of adversarial operations relative to the resources they expend. Overall, this work bridges the gap between Byzantine-Tolerant CRDTs and resource-bounded adversarial models, providing a principled foundation for deploying CRDTs in fully open, adversarial environments. © 2026 Copyright held by the owner/author(s).

2026

“It Makes the Code Clearer”: Why Developers Adopt ModernPython Features in Open Source Projects

Authors
Mendonça, W; Leite, M; Romeiro, O; Carvalho, F; Bonifácio, R; Monteiro, E; Pinto, G; Accioly, P; Saraiva, J;

Publication

Abstract
Python has become one of the most widely used programming languages, yet the transition fromPython 2 to 3 introduced a tension between innovation and compatibility. While new featuressuch as formatted string literals, type annotations, and structural pattern matching expanded thelanguage’s expressiveness, they also required substantial adaptation of legacy code. Despite theincreasing relevance of these features, there is still limited empirical evidence on how modernPython features are being adopted in practice—when developers start using them, how adoptionunfolds over time, and what motivations drive these decisions. This paper addresses this gapthrough a large-scale empirical study of 424 open-source Python projects. Our analysis revealstwo distinct adoption patterns: rapid adoption of small syntactic improvements and slowerintegration of features that require extensive refactoring or ecosystem support. On average,projects begin using with new features within 16 months after their release but take roughly 4years to achieve broader and sustained adoption. This observation may be partially explainedby the transition from Python 2 to 3, which did not preserve full backward compatibility.Complementary qualitative evidence from pull-request discussions indicates that developers areprimarily motivated to rejuvenate Python code through improvements in comprehension, safety,and performance, yet often constrained by compatibility requirements and maintenance costs.Together, these findings offer practical insights for tool developers and maintainers seeking tobalance innovation and stability in the ongoing rejuvenation of Python source code.

2026

Foreword to the special section on recent advances in graphics and interaction (RAGI 2025)

Authors
Alves, T; Campos, JC; Chalmers, A;

Publication
COMPUTERS & GRAPHICS-UK

Abstract
[No abstract available]