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 reinforces EU–Brazil cooperation in supercomputing and quantum technologies

INESC TEC joined the international workshop Identifying potential core areas of HPC cooperation between the EU and Brazil, held at the Laboratório Nacional de Computação Científica (LNCC) in Petrópolis, Brazil. The event was organised by the Brazilian Ministry of Science, Technology and Innovation (MCTI) and the Delegation of the European Union to Brazil, and brought together researchers, policy-makers, scientific decision-makers and industry representatives to identify strategic areas for cooperation between the European Union and Brazil in the fields of high-performance computing (HPC) and quantum technologies. 

21st January 2026

Computer Science and Engineering

BANKSY project kicks off to revolutionise reasoning over vague and contradictory information

The BANKSY project, funded by the Portuguese Foundation for Science and Technology (FCT), promises to innovate the way we deal with contexts characterised by incomplete, uncertain or even contradictory information. With a planned duration of three years, the project is the result of a partnership between INESC TEC, CIDMA, the University of Aveiro and AIBILI (Association for Innovation and Biomedical Research on Light and Image). 

16th December 2025

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

004

Projects

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

QuantumCLP

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

2025-2027

BigHPC

A Management Framework for Consolidated Big Data and HPC

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

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

2026

Engineering Methods for HCI and UX in AI-Driven Systems

Authors
Spano, LD; Palanque, P; Martinie, C; Campos, JC; Schmidt, A; Barricelli, BR; ElAgroudy, P; Luyten, K;

Publication
HUMAN-COMPUTER INTERACTION - INTERACT 2025, PT IV

Abstract
The growing integration of Artificial Intelligence (AI) into interactive systems presents unique challenges and opportunities for Human-Computer Interaction (HCI) and User Experience (UX). While AI can enhance usability and provide novel interaction paradigms, it also raises concerns related to transparency, control, and user trust. This workshop seeks to bring together researchers and practitioners to discuss state-of-the-art engineering methods that support HCI and UX in AI-driven systems. By fostering interdisciplinary collaboration, we aim to identify key challenges, share best practices, and develop a roadmap for future research in this critical area.

2026

Towards a More Natural Approach to Property Specification in the IVY Workbench

Authors
Gomes, J; Arcipreste, M; Gomes, M; Campos, JC;

Publication
HUMAN-COMPUTER INTERACTION - INTERACT 2025, PT III

Abstract
Safety-critical interactive systems pose design and evaluation challenges that go beyond usability. The safety of the system (i.e. the guarantee that it does not reach an undesirable or incorrect state) is also a relevant consideration. Traditional user-centred approaches (UCD) lack the rigour and thoroughness needed to address safety, and formal verification arises as a possible solution. Applying formal verification to a safety-critical interactive system design encompasses developing a model, expressing and verifying properties, and analysing the verification results. In the case of model checking, properties are typically expressed in temporal logic. This creates a gap between the languages used in UCD and the languages used for formal verification. Creating temporal logic properties manually requires expertise in formal methods and can be both time-consuming and error-prone. This paper explores how a patterns-based approach can be used to support the specification of properties in a natural language-based style. A prototype implementation of the approach is evaluated through a user study, and the results of this evaluation are discussed.

2026

On Quantitative Solution Iteration in QAlloy

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

Publication
RIGOROUS STATE-BASED METHODS, ABZ 2025

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.

Facts & Figures

1R&D Employees

2020

68Researchers

2016

14Proceedings in indexed conferences

2020

Contacts