Cookies
O website necessita de alguns cookies e outros recursos semelhantes para funcionar. Caso o permita, o INESC TEC irá utilizar cookies para recolher dados sobre as suas visitas, contribuindo, assim, para estatísticas agregadas que permitem melhorar o nosso serviço. Ver mais
Aceitar Rejeitar
  • Menu
Apresentação

Laboratório de Software Confiável

No Laboratório de Software Confiável (HASLab), melhorando a prática através da teoria, criamos e implementamos software que vai além da funcionalidade: garantimos que é correto, resiliente e seguro contra falhas e ataques.


A nossa equipa de investigadores, cientistas e engenheiros tem competências em engenharia de software, onde desenvolvemos métodos e ferramentas para conceber e integrar software robusto; sistemas distribuídos, onde exploramos a distribuição e replicação para garantir escalabilidade e confiabilidade; e segurança da informação, onde considerando também os desafios da cibersegurança, fortalecemos os sistemas com protocolos criptográficos avançados e seguros, minimizando vulnerabilidades.


Com uma abordagem multidisciplinar e sustentada por princípios teóricos sólidos, criamos soluções inovadoras para software crítico, infraestruturas cloud seguras e gestão de big data com privacidade, impulsionando avanços científicos, inovação e consultoria de excelência.


Além disso, complementamos a nossa expertise em áreas como interação humano-computador, linguagens de programação, matemática de computação e computação quântica - porque acreditamos que o futuro do software confiável se constrói com conhecimento e inovação.

Tópicos
de interesse
081

Projetos em destaque

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

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

QuantumCLP

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

2025-2027

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

TestBed5G_Robotics

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

2025-2025

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

Financiamento Bolsas Doutoramento FCT - Gestão

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 - Sistema Modular de Armazenamento e Gestão de Dados em Blockchain com IA

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

Aliança para a Transição Energética

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

Investigação do Impacto de Verificação Formal na Adopção de Software para Segurança de Passwords

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

BigHPC

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

Sistemas descentralizados confiáveis e escaláveis suportados por hardware

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

Architecturas distribuídas: variabilidade e interação de sistemas ciber-físicos

2018-2022

SAFER

Verificação de segurança para software robótico

2018-2021

KLEE

Modelação coalgébrica e análise para biologia sintética computacional

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: Computação Verde como uma Disciplina de Engenharia

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

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

Análise Integrada e Visual de Big Data Ultra-escalável e Ultra-eficiente

2014-2017

Practice

Ferramentas de Preservação de Privacidade na Cloud

2013-2016

CoherentPaaS

PaaS Rica e Coerente com um Modelo de Programação Comum

2013-2016

Equipa
  • a
  • b
  • c
  • d
  • e
  • f
  • g
  • h
  • i
  • j
  • k
  • l
  • m
  • n
  • o
  • p
  • q
  • r
  • s
  • t
  • u
  • v
  • w
  • x
  • y
  • z
Publicações

HASLab Publicações

Ler todas as publicações

2026

Auto-active verification of distributed systems and specification refinements with Why3-do

Autores
Lourenço, CB; Pinto, JS;

Publicação
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)

Autores
Alves, T; Campos, JC; Chalmers, A;

Publicação
COMPUTERS & GRAPHICS-UK

Abstract

2026

Engineering Methods for HCI and UX in AI-Driven Systems

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

Publicação
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

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

Publicação
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

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

Publicação
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.