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
Facts & Numbers
000
Presentation

High-Assurance Software

HASLab is focused on the design and implementation of high-assurance software systems: software that is correct by design and resilient to environment faults and malicious attacks. 

To accomplish this mission, HASLab covers three main competences — Cybersecurity, Distributed Systems, and Software Engineering — complemented by other competences such as Human-Computer Interaction, Programming Languages, or the Mathematics of Computing. 

Software Engineering – methods, techniques, and tools for rigorous software development, that can be applied to the internal functionality of a component, its composition with other components, as well as the interaction with the user.

Distributed Systems – improving the reliability and scalability of software, by exploring properties inherent to the distribution and replication of computer systems.

Cybersecurity – minimize the vulnerability of software components to hostile attacks, by deploying structures and cryptographic protocols whose security properties are formally proven.

Through a multidisciplinary approach that is based on solid theoretical foundations, we aim to provide solutions — theory, methods, languages, tools — for the development of complete ICT systems that provide strong guarantees to their owners and users. Prominent application areas of HASLab research include the development of safety and security critical software systems, the operation of secure cloud infrastructures, and the privacy-preserving management and processing of big data.

Latest News
Computer Science and Engineering

INESC TEC strengthened international position with new contributions in the field of storage systems and networks

Last month, the Institute participated in two of the most prestigious international conferences in databases and networks – VLDB and SIGCOMM. The researchers brought to the international debate new frontiers in storage, fault tolerance, and operating systems. 

29th October 2025

Computer Science and Engineering

INESC TEC researchers developed a new hybrid algorithm that improves the reliability of quantum computing

INESC TEC researchers have developed a new hybrid quantum–classical algorithm that promises to make quantum computing more practical and resilient to the challenges posed by current quantum devices. The research work “Bayesian Quantum Amplitude Estimation” proposes an innovative approach to one of the fundamental tasks in quantum computing – amplitude estimation – with applications in fields like engineering, finance, and Artificial Intelligence. 

29th October 2025

Computer Science and Engineering

INESC TEC hosts meeting of international group of experts on algorithmic languages and formal calculi

Nearly 30 world-renowned experts from around the world travelled to Portugal to discuss advances in the fields of computer science theory and programming languages. Members of the IFIP Working Group 2.1 on Algorithmic Languages and Calculi gathered in Viana do Castelo for an initiative organised by INESC TEC. 

07th October 2025

INESC TEC research on data replication boosts international impact in distributed systems

An INESC TEC research on data replication in relational databases received an honourable mention at SIGMOD 2025, one of the leading international conferences in the field of data management – ranking among the four best papers out of 250 submissions. 

28th July 2025

Computer Science and Engineering

INESC TEC researcher won Amazon Research Award

Alexandra Mendes, a researcher at INESC TEC, received the Amazon Research Award in automated reasoning. This is the first time this award has been granted to researchers who carry out their R&D work in Portugal.

27th June 2025

016

Projects

ADAPQO

Adaptive Query Optimization Architectures to Support Heterogeneous Data Intensive Applications

2025-2026

QUANTHOS

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

2025-2027

JasminCode

Developing Reliable High-performance Assembly Code using Jasmin

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

ATAI

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

2025-2027

DisaggregatedHPC

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

2025-2026

PFAI4_6eD

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

2025-2025

InfraGov

InfraGov: A Public Framework for Reliable and Secure IT Infrastructure

2025-2026

VeriFixer

VeriFixer: Automated Repair for Verification-Aware Programming Languages

2025-2026

BolsasFCT_Gestao

Funding FCT PhD Grants - Management

2025-9999

ENSCOMP4

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

2024-2025

PFAI4_5eD

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

2024-2024

QuantELM

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

2023-2024

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

Team
001

Laboratory

CLOUDinha

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

On Quantitative Solution Iteration in QAlloy

Authors
Silva, P; Macedo, N; Oliveira, JN;

Publication
Lecture Notes in Computer Science

Abstract
A key feature of model finding techniques allows users to enumerate and explore alternative solutions. However, it is challenging to guarantee that the generated instances are relevant to the user, representing effectively different scenarios. This challenge is exacerbated in quantitative modelling, where one must consider both the qualitative, structural part of a model, and the quantitative data on top of it. This results in a search space of possibly infinite candidate solutions, often infinitesimally similar to one another. Thus, research on instance enumeration in qualitative model finding is not directly applicable to the quantitative context, which requires more sophisticated methods to navigate the solution space effectively. The main goal of this paper is to explore a generic approach for navigating quantitative solution spaces and showcase different iteration operations, aiming to generate instances that differ considerably from those previously seen and promote a larger coverage of the search space. Such operations are implemented in QAlloy – a quantitative extension to Alloy – on top of Max-SMT solvers, and are evaluated against several examples ranging, in particular, over the integer and fuzzy domains. © 2025 Elsevier B.V., All rights reserved.

2026

A framework for supporting the reproducibility of computational experiments in multiple scientific domains

Authors
Costa, L; Barbosa, S; Cunha, J;

Publication
Future Gener. Comput. Syst.

Abstract
In recent years, the research community, but also the general public, has raised serious questions about the reproducibility and replicability of scientific work. Since many studies include some kind of computational work, these issues are also a technological challenge, not only in computer science, but also in most research domains. Computational replicability and reproducibility are not easy to achieve due to the variety of computational environments that can be used. Indeed, it is challenging to recreate the same environment via the same frameworks, code, programming languages, dependencies, and so on. We propose a framework, known as SciRep, that supports the configuration, execution, and packaging of computational experiments by defining their code, data, programming languages, dependencies, databases, and commands to be executed. After the initial configuration, the experiments can be executed any number of times, always producing exactly the same results. Our approach allows the creation of a reproducibility package for experiments from multiple scientific fields, from medicine to computer science, which can be re-executed on any computer. The produced package acts as a capsule, holding absolutely everything necessary to re-execute the experiment. To evaluate our framework, we compare it with three state-of-the-art tools and use it to reproduce 18 experiments extracted from published scientific articles. With our approach, we were able to execute 16 (89%) of those experiments, while the others reached only 61%, thus showing that our approach is effective. Moreover, all the experiments that were executed produced the results presented in the original publication. Thus, SciRep was able to reproduce 100% of the experiments it could run. © 2025 The Authors

2025

Uma extensão de Raft com propagação epidémica

Authors
Gonçalves, A; Alonso, AN; Pereira, J; Oliveira, R;

Publication
CoRR

Abstract

2025

Social Compliance With NPIs, Mobility Patterns, and Reproduction Number: Lessons From COVID-19 in Europe

Authors
Baccega, D; Aguilar, J; Baquero, C; Anta, AF; Ramirez, JM;

Publication
IEEE ACCESS

Abstract
Non-pharmaceutical interventions (NPIs), such as lockdowns, travel restrictions, and social distancing mandates, play a critical role in controlling the spread of infectious diseases by shaping human mobility patterns. Using COVID-19 as a case study, this research investigates the relationships between NPIs, mobility, and the effective reproduction number (R-t) across 13 European countries. We employ XGBoost regression models to estimate missing mobility data from NPIs and missing R(t )values from mobility, achieving high accuracy. Additionally, using clustering techniques, we uncover national distinctions in social compliance. Northern European countries demonstrate higher adherence to NPIs than Southern Europe, which exhibits more variability in response to restrictions. These differences highlight the influence of cultural and social norms on public health outcomes. In general, our analysis reveals a strong correlation between NPIs and mobility reductions, highlighting the immediate impact of restrictions on population movement. However, the relationship between mobility and R(t )is weaker and more nuanced, reflecting the time delays involved, as changes in mobility take time to influence transmission rates. These results underscore the interdependence of restrictions, mobility, and disease spread while demonstrating the potential for data-driven approaches to guide policy decisions. Our approach offers valuable insights for optimizing public health strategies and tailoring interventions to diverse cultural contexts during future health crises.

Facts & Figures

16Academic Staff

2020

1R&D Employees

2020

68Researchers

2016

Contacts