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
Computer Science and Engineering

INESC TEC joins Iberian consortium to advence quantum computing and Artificial Intelligence

Turning the Iberian Peninsula into a European benchmark for quantum technologies and AI - that is the goal of Quantum IberIA, a cross-border cooperation project bringing together 17 entities from both countries, including INESC TEC. 

26th June 2026

Computer Science and Engineering

Security of public service portals put to the test: INESC TEC researchers take results to several stages

From assessing Portuguese municipal councils to evaluating more than 3000 public service portals worldwide, the work of INESC TEC researchers Diogo Ribeiro and João Marco Silva puts the cybersecurity of public administration at the centre of the debate. 

19th June 2026

Computer Science and Engineering

INESC TEC with strong presence at EuroSys 2026

From a best poster award to contributions on four distinct fronts. That is how INESC TEC made its mark at EuroSys 2026, one of the most prestigious international conferences in computer systems.

15th June 2026

INESC TEC researcher joins board of international graph database organisation

Nuno Faria, a researcher at INESC TEC, has joined the board of the Graph Data Council (GDC), a leading international non-profit organisation in the field of graph databases. Faria, who is also a guest lecturer at the School of Engineering of the University of Minho, is the only Portuguese member on the GDC board, which includes representatives from companies such as Microsoft, Oracle, and AWS. 

31st March 2026

Computer Science and Engineering

INESC TEC reinforced international position in HPC at CENTRA 9 and consolidated transnational collaborations

INESC TEC took part in CENTRA 9, a meeting of the international CENTRA (Collaborations to Enable Transnational Cyberinfrastructure Applications) network, which brings together research centres, institutes and laboratories from various regions to advance transnational cyberinfrastructures and their applications – a critical pillar for the progress of high-performance computing (HPC) and associated ecosystems. 

24th February 2026

Interest
Topics
035

Featured Projects

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

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

INSIEME

Integrated Network for data Space and Interoperable Energy Management in Europe

2025-2028

InfraGov

InfraGov: A Public Framework for Reliable and Secure IT Infrastructure

2025-2026

VeriFixer

VeriFixer: Automated Repair for Verification-Aware Programming Languages

2025-2027

CDMS

Claim Denial Management Solution

2025-2026

ENSCOMP4

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

2024-2026

PeT

PeT - Privacidade e Transparência

2024-2028

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

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

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

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

IDINA

Identidade Digital Inclusiva Não Autoritativa

2021-2025

DigiLightRail

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

2020-2023

InterConnect

Interoperable Solutions Connecting Smart Homes, Buildings and Grids

2019-2024

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]