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

In the era of pervading data storage, replication can be the key to large-scale systems. Here’s how a INESC TEC research explores these challenges

In a study published in ACM Computing Surveys, Paulo Sérgio Almeida, INESC TEC researcher, synthesises the existing knowledge on approaches to Conflict-free Replicated Data Types, a topic he has been exploring over the past decade. These enable replication in distributed systems with automatic conflict resolution, ensuring high availability – even in the face of communication failures.

04th October 2024

INESC TEC with five FCT exploratory projects approved in four R&D areas

Telecommunications and Multimedia, Applied Photonics, High-assurance Software and Advanced Computing Systems – these are the four domains that INESC TEC researchers will explore within the scope of the five projects that were approved through the Call for Exploratory Projects promoted by the Foundation for Science and Technology (FCT).

02nd October 2024

Computer Science and Engineering

Edge databases have many benefits — and INESC TEC researchers have dedicated themselves to studying them

The paper Databases in Edge and Fog Environments: A Survey, signed by Luís Manuel Ferreira, Fábio Coelho and José Orlando Pereira - and published in ACM Computing Surveys -, establishes innovative concepts in the edge databases area, resorting to several publications on hardware used, latency performance, energy consumption and privacy. This new type of database benefits from devices close to the users to improve performance and features.

03rd July 2024

Computer Science and Engineering

Researcher at INESC TEC wins an award thanks to prototype to support the development of Defense policies and strategies

Alexandra Mendes, INESC TEC researcher, is one of the winners of the Atlantic Security Award, promoted by FLAD; Alexandra’s work aims to use a large language model – trained with data retrieved from the dark web – in decision-making processes, in the design of Defense policies and strategies, and in the application of the law in the security of the Atlantic region.

28th May 2024

Computer Science and Engineering

INESC TEC researchers propose innovative cryptography solution for potential quantum computers threats

The solution proposed by Manuel Barbosa and João Barbosa, researchers at INESC TEC, features a hybrid key-encapsulation mechanism (KEM), capable of addressing the demands of the dynamics of hybrid models that combine pre-quantum and post-quantum algorithms.

21st May 2024

006

Projects

BringTrust

Strengthening CI/CD Pipeline Cybersecurity and Safeguarding the Intellectual Property

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

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

Alloy Repair Hint Generation Based on Historical Data

Authors
Barros, A; Neto, H; Cunha, A; Macedo, N; Paiva, ACR;

Publication
FORMAL METHODS, PT II, FM 2024

Abstract
Platforms to support novices learning to program are often accompanied by automated next-step hints that guide them towards correct solutions. Many of those approaches are data-driven, building on historical data to generate higher quality hints. Formal specifications are increasingly relevant in software engineering activities, but very little support exists to help novices while learning. Alloy is a formal specification language often used in courses on formal software development methods, and a platform-Alloy4Fun-has been proposed to support autonomous learning. While non-data-driven specification repair techniques have been proposed for Alloy that could be leveraged to generate next-step hints, no data-driven hint generation approach has been proposed so far. This paper presents the first data-driven hint generation technique for Alloy and its implementation as an extension to Alloy4Fun, being based on the data collected by that platform. This historical data is processed into graphs that capture past students' progress while solving specification challenges. Hint generation can be customized with policies that take into consideration diverse factors, such as the popularity of paths in those graphs successfully traversed by previous students. Our evaluation shows that the performance of this new technique is competitive with non-data-driven repair techniques. To assess the quality of the hints, and help select the most appropriate hint generation policy, we conducted a survey with experienced Alloy instructors.

2025

Promoting sustainable and personalized travel behaviors while preserving data privacy

Authors
Brito C.; Pina N.; Esteves T.; Vitorino R.; Cunha I.; Paulo J.;

Publication
Transportation Engineering

Abstract
Cities worldwide have agreed on ambitious goals regarding carbon neutrality. To do so, policymakers seek ways to foster smarter and cleaner transportation solutions. However, citizens lack awareness of their carbon footprint and of greener mobility alternatives such as public transports. With this, three main challenges emerge: (i) increase users’ awareness regarding their carbon footprint, (ii) provide personalized recommendations and incentives for using sustainable transportation alternatives and, (iii) guarantee that any personal data collected from the user is kept private. This paper addresses these challenges by proposing a new methodology. Created under the FranchetAI project, the methodology combines federated Artificial Intelligence (AI) and Greenhouse Gas (GHG) estimation models to calculate the carbon footprint of users when choosing different transportation modes (e.g., foot, car, bus). Through a mobile application that keeps the privacy of users’ personal information, the project aims at providing detailed reports to inform citizens about their impact on the environment, and an incentive program to promote the usage of more sustainable mobility alternatives.

2025

Modelling sustainability in cyber-physical systems: A systematic mapping study

Authors
Barisic, A; Cunha, J; Ruchkin, I; Moreira, A; Araújo, J; Challenger, M; Savic, D; Amaral, V;

Publication
SUSTAINABLE COMPUTING-INFORMATICS & SYSTEMS

Abstract
Supporting sustainability through modelling and analysis has become an active area of research in Software Engineering. Therefore, it is important and timely to survey the current state of the art in sustainability in Cyber-Physical Systems (CPS), one of the most rapidly evolving classes of complex software systems. This work presents the findings of a Systematic Mapping Study (SMS) that aims to identify key primary studies reporting on CPS modelling approaches that address sustainability over the last 10 years. Our literature search retrieved 2209 papers, of which 104 primary studies were deemed relevant fora detailed characterisation. These studies were analysed based on nine research questions designed to extract information on sustainability attributes, methods, models/meta-models, metrics, processes, and tools used to improve the sustainability of CPS. These questions also aimed to gather data on domain-specific modelling approaches and relevant application domains. The final results report findings for each of our questions, highlight interesting correlations among them, and identify literature gaps worth investigating in the near future.

2025

The CAOS framework for Scala: Computer-aided design of SOS

Authors
Proença, J; Edixhoven, L;

Publication
SCIENCE OF COMPUTER PROGRAMMING

Abstract
We present Caos: a programming framework for computer-aided design of structural operational semantics for formal models. This framework includes a set of Scala libraries and a workflow to produce visual and interactive diagrams that animate and provide insights over the structure and the semantics of a given abstract model with operational rules. Caos follows an approach where theoretical foundations and a practical tool are built together, as an alternative to foundations-first design (tool justifies theory) or tool-first design (foundations justify practice). The advantage of Caos is that the tool-under-development can immediately be used to automatically run numerous and sizeable examples in order to identify subtle mistakes, unexpected outcomes, and unforeseen limitations in the foundations-under-development, as early as possible. More concretely, Caos supports the quick creation of interactive websites that help the end-users better understand a new language, structure, or analysis. End-users can be research colleagues trying to understand a companion paper or students learning about a new simple language or operational semantics. We include a list of open-source projects with a web frontend supported by Caos that are used both in research and teaching contexts.

2025

Logic and Calculi for All on the occasion of Luis Barbosa's 60th birthday

Authors
Madeira, A; Oliveira, JN; Proença, J; Neves, R;

Publication
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING

Abstract
[No abstract available]

Facts & Figures

68Researchers

2016

0Book Chapters

2020

16Academic Staff

2020

Contacts