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

INESC TEC and Carnegie Mellon University join forces to create the next generation of database optimisers

At a time when the complexity and popularity of data-driven applications are growing at an unprecedented rate, INESC TEC and Carnegie Mellon University (CMU) are collaborating on a project to tackle one of the most debated challenges in the field: the efficiency of the data-processing systems that support these applications. The project, called ADAPQO, aims to transform the way databases make decisions.  In modern database systems, the optimiser is the component responsible for determining the best way to execute each user query. Faced with millions of potential alternatives, this decision has become increasingly difficult, with a direct impact on performance and system efficiency - especially in a context where the diversity of databases is expanding to meet the needs of new Artificial Intelligence (AI) applications.  To address this challenge, ADAPQO aims to develop a new type of optimiser capable of learning from experience and continuously improving decision-making capabilities. “The vision is to create an autonomous service that collects knowledge over time and can be easily integrated into different data management systems,” said José Orlando Pereira. “Beyond the technological impact, the initiative is also expected to accelerate research and boost advanced training in the field of databases,” added the researcher, who is also a professor at the University of Minho.  Building on an already well-established research line at INESC TEC, the Institute is represented by José Orlando Pereira, Ana Nunes Alonso and Nuno Faria, INESC TEC researchers in databases, who coordinate the Portuguese component of the project and participate actively in the scientific and technological development. Concerning the U.S.A., the project involves the collaboration of Andy Pavlo, leader of the CMU Database Group and an international reference in the field.  The researchers mentioned in this news piece are associated with INESC TEC and UMinho.

11th December 2025

Computer Science and Engineering

Quien sabe por Algebra, sabe scientificamente” – the retirement of José Nuno Oliveira marks an era in Computer Science at UMinho

More than four decades have passed since José Nuno Oliveira first stepped into the University of Minho (UMinho). On 14 November, Auditorium A1 at the Gualtar Campus in Braga was the setting for a farewell that stirred emotions and memories. The UMinho community – and beyond – gathered to celebrate José Nuno Oliveira’s dedication to teaching, research, and the training of generations in Computer Engineering.   

28th November 2025

INESC TEC positions national supercomputing at the forefront of Europe

INESC TEC has once again placed itself at the heart of European decision-making – this time in the field of supercomputing. On 10 November, the European Commission’s Executive Vice-President, Henna Virkkunen, visited the Deucalion supercomputer, installed at the University of Minho (UMinho), in Guimarães. The visit highlighted Portugal’s contribution to the European Union’s digital and scientific strategy in this domain. 

27th November 2025

Computer Science and Engineering

INESC TEC participated in a debate on the future of data centres in Portugal

What steps must be taken to ensure sustainable and efficient data centres in Portugal? And what role can supercomputing play in this process? INESC TEC took part in an initiative organised by APDC – Digital Business Community, in collaboration with VdA and Portugal Data Centers, to discuss the installation, operation and future of these infrastructures in the country.

26th November 2025

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

077

Projects

POISE

Programmable Asynchronous Asymmetric Secure Choreographies

2025-2027

QUANTHOS

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

2025-2027

ADAPQO

Adaptive Query Optimization Architectures to Support Heterogeneous Data Intensive Applications

2025-2026

TestBed5G_Robotics

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

2025-2025

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

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

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

21Senior Researchers

2016

0Book Chapters

2020

4Papers in indexed journals

2020

Contacts