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

Greener high-performance computing? INESC TEC is processing solutions – and the keyword is “disaggregation”

Underused resources, wasted energy, and high operational costs. INESC TEC is leading a project that aims to propose alternatives to how computing resources are organised and managed.

05th May 2025

INESC TEC researchers strengthened the partnership with CENTRA international network

INESC TEC reaffirmed the institution’s commitment to international research collaboration by participating in the CENTRA 2025 event, a global initiative that brings together research centres, institutes, and laboratories from across the world to drive the development of transnational cyberinfrastructures. This year’s edition focused on Artificial Intelligence (AI), exploring application in linguistics, cognitive psychology and advanced management of cyberinfrastructures. 

28th March 2025

Computer Science and Engineering

Advanced computing as a bridge between Portugal and Japan: INESC TEC and AIST reinforce scientific cooperation

Five years have passed since INESC TEC and the National Institute of Advanced Industrial Science and Technology (AIST), in Japan, signed the first Memorandum of Understanding (MoU). This scientific cooperation agreement, focused on advanced computing, led to major opportunities for mobility, joint publications and the exchange of knowledge and experiences, thus bringing the Portuguese and Japanese R&D ecosystems closer together – particularly in High-Performance Computing (HPC). Recently, the two institutes renewed the MoU and will continue to work together to boost research in advanced computing.

03rd February 2025

Computer Science and Engineering

There are bridges uniting biomedical engineering and supercomputing - INESC TEC researchers flew to Barcelona to cross them

For a week, Alicia Oliveira and Beatriz Cepa left INESC TEC's laboratories in Braga and went to Barcelona - the city that welcomed the ACM Summer School. The researchers explored some of the elemental HPC concepts and realised that - in a context dominated by computer science - their training in biomedical engineering was an asset.

31st October 2024

Computer Science and Engineering

Software bugs are as persistent as those in nature - a study by INESC TEC closed in on them

INESC TEC researchers developed the LazyFS tool, capable of injecting faults and reproducing data loss bugs. The solution helps to understand the origin and cause of said bugs, but also to validate protection mechanisms against failures. 

07th October 2024

005

Projects

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

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

Team
001

Laboratory

CLOUDinha

Publications

HASLab Publications

View all Publications

2025

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

Authors
Baccega, D; Aguilar, J; Baquero, C; Fernández Anta, A; Ramirez, JM;

Publication

Abstract
AbstractNon-pharmaceutical interventions (NPIs), including measures such as lockdowns, travel limitations, and social distancing mandates, play a critical role in shaping human mobility, which subsequently influences the spread of infectious diseases. Using COVID-19 as a case study, this research examines the relationship between restrictions, mobility patterns, and the disease’s effective reproduction number (Rt) across 13 European countries. Employing clustering techniques, we uncover distinct national patterns, highlighting differences in social compliance between Northern and Southern Europe. While restrictions strongly correlate with mobility reductions, the relationship between mobility and Rtis more nuanced, driven primarily by the nature of social interactions rather than mere compliance. Additionally, employing XGBoost regression models, we demonstrate that missing mobility data can be accurately inferred from restrictions, and missing infection rates can be predicted from mobility data. These findings provide valuable insights for tailoring public health strategies in future crisis and refining analytical approaches.

2025

Leakage-Free Probabilistic Jasmin Programs

Authors
Almeida, JB; Firsov, D; Oliveira, T; Unruh, D;

Publication
PROCEEDINGS OF THE 14TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2025

Abstract
This paper presents a semantic characterization of leakage-freeness through timing side-channels for Jasmin programs. Our characterization covers probabilistic Jasmin programs that are not constant-time. In addition, we provide a characterization in terms of probabilistic relational Hoare logic and prove the equivalence between both definitions. We also prove that our new characterizations are compositional and relate our new definitions to existing ones from prior work, which could only be applied to deterministic programs. To provide practical evidence, we use the Jasmin framework to develop a rejection sampling algorithm and provide an EasyCrypt proof that ensures the algorithm's implementation is leakage-free while not being constant-time.

2025

CRDV: Conflict-free Replicated Data Views

Authors
Faria, N; Pereira, J;

Publication
Proc. ACM Manag. Data

Abstract
There are now multiple proposals for Conflict-free Replicated Data Types (CRDTs) in SQL databases aimed at distributed systems. Some, such as ElectricSQL, provide only relational tables as convergent replicated maps, but this omits semantics that would be useful for merging updates. Others, such as Pg\_crdt, provide access to a rich library of encapsulated column types. However, this puts merge and query processing outside the scope of the query optimizer and restricts the ability of an administrator to influence access paths with materialization and indexes. Our proposal, CRDV, overcomes this challenge by using two layers implemented as SQL views: The first provides a replicated relational table from an update history, while the second implements varied and rich types on top of the replicated table. This allows the definition of merge semantics, or even entire new data types, in SQL itself, and enables global optimization of user queries together with merge operations. Therefore, it naturally extends the scope of query optimization and local transactions to operations on replicated data, can be used to reproduce the functionality of common CRDTs with simple SQL idioms, and results in better performance than alternatives.

2025

Specification of paraconsistent transition systems, revisited

Authors
Cunha, J; Madeira, A; Barbosa, LS;

Publication
SCIENCE OF COMPUTER PROGRAMMING

Abstract
The need for more flexible and robust models to reason about systems in the presence of conflicting information is becoming more and more relevant in different contexts. This has prompted the introduction of paraconsistent transition systems, where transitions are characterized by two pairs of weights: one representing the evidence that the transition effectively occurs and the other its absence. Such a pair of weights can express scenarios of vagueness and inconsistency. . This paper establishes a foundation for a compositional and structured specification approach of paraconsistent transition systems, framed as paraconsistent institution. . The proposed methodology follows the stepwise implementation process outlined by Sannella and Tarlecki.

2025

Approaches to Conflict-free Replicated Data Types

Authors
Almeida, PS;

Publication
ACM COMPUTING SURVEYS

Abstract
Conflict-free Replicated Data Types (CRDTs) allow optimistic replication in a principled way. Different replicas can proceed independently, being available even under network partitions and always converging deterministically: Replicas that have received the same updates will have equivalent state, even if received in different orders. After a historical tour of the evolution from sequential data types to CRDTs, we present in detail the two main approaches to CRDTs, operation-based and state-based, including two important variations, the pure operation-based and the delta-state based. Intended for prospective CRDT researchers and designers, this article provides solid coverage of the essential concepts, clarifying some misconceptions that frequently occur, but also presents some novel insights gained from considerable experience in designing both specific CRDTs and approaches to CRDTs.

Facts & Figures

14Proceedings in indexed conferences

2020

21Senior Researchers

2016

1R&D Employees

2020

Contacts