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
Factos & Números
000
Apresentação

Laboratório de Software Confiável

O HASLab dedica-se à criação e à implementação de sistemas de software confiável, i.e., software correto e resiliente perante falhas e ataques.

De forma a cumprir este grande objetivo, o HASLab opera em três grandes áreas - Cibersegurança, Sistemas Distribuídos e Engenharia de Software.

Engenharia de Software - são explorados métodos, técnicas e ferramentas para o desenvolvimento de software, podendo este ser integrado nas funcionalidades internas de determinados componentes, na sua configuração junto de outros componentes, e também na interação com o utilizador.

Sistemas Distribuídos - com vista a melhorar a confiabilidade e a escalabilidade de software, explorando as propriedades inerentes à distribuição e à replicação de sistemas computacionais.

Cibersegurança - de forma a minimizar a vulnerabilidade dos componentes de software a ataques, com recurso à implementação de estruturas e de protocolos criptográficos com propriedades de segurança formalmente comprovadas.

Através de uma abordagem multidisciplinar que assenta em princípios teóricos comprovados, o HASLab visa disponibilizar soluções - fundamentos teóricos, métodos, linguagens, ferramentas - para o desenvolvimento de sistemas TIC abrangentes, dando garantias aos seus proprietários e utilizadores. Os grandes domínios de aplicação da investigação desenvolvida no HASLab incluem o desenvolvimento de sistemas de software cruciais para garantir a segurança e a proteção, a operacionalização de infraestruturas da nuvem seguras, e a gestão e o tratamento de big data, tendo em conta as questões da privacidade.

Últimas Notícias
Ciência e Engenharia dos Computadores

INESC TEC acolhe reunião de grupo internacional de especialistas no estudo e desenvolvimento de linguagens algorítmicas e cálculos formais

Quase 30 especialistas de renome mundial, provenientes de vários pontos do globo, rumaram a Portugal para discutir os avanços na área da teoria da computação e das linguagens de programação. Os membros do IFIP Working Group 2.1 on Algorithmic Languages and Calculi estiveram reunidos em Viana do Castelo, numa iniciativa organizada pelo INESC TEC.  

07 outubro 2025

Investigação INESC TEC sobre replicação de dados reforça impacto internacional em sistemas distribuídos

Investigação do INESC TEC sobre replicação de dados em bases de dados relacionais foi, recentemente, distinguida com uma menção honrosa na SIGMOD 2025, uma das principais conferências internacionais na área de gestão de dados, posicionando-se entre os quatro melhores artigos da conferência dos 250 submetidos. 

28 julho 2025

Ciência e Engenharia dos Computadores

Investigadora do INESC TEC é premiada com o Amazon Research Award

Alexandra Mendes, investigadora do INESC TEC, acaba de receber o Amazon Research Award, na área de automated reasoning. É a primeira vez que este prémio é atribuído a investigadores que desenvolvem os seus trabalhos de I&D em Portugal.

27 junho 2025

Supercomputação mais “verde”? O INESC TEC está a processar soluções – e a palavra-chave é “desagregar”

Recursos subaproveitados, energia desperdiçada e custos operacionais elevados. O INESC TEC lidera um projeto que quer propor alternativas à forma como os recursos computacionais são organizados e geridos.

05 maio 2025

Investigadores INESC TEC reforçam parceria com rede internacional CENTRA

O INESC TEC reafirmou o seu compromisso com a colaboração internacional em investigação ao participar no evento CENTRA 2025, uma iniciativa global que reúne centros de investigação, institutos e laboratórios das várias partes do mundo para impulsionar o desenvolvimento de ciberinfraestruturas transnacionais. Esta edição do evento focou-se na área da Inteligência Artificial (IA), explorando a sua aplicação na linguística, na psicologia cognitiva e na gestão avançada de ciberinfraestruturas. 

28 março 2025

060

Projetos Selecionados

BANSKY

A paraconsistent inference engine to support research in age-ralated molecular degeneration

2025-2028

INSIEME

Integrated Network for data Space and Interoperable Energy Management in Europe

2025-2028

JRCSIF

JRC Interoperability Laboratory Adoption of the Semantic Interoperability Framework

2025-2025

CDMS

Claim Denial Management Solution

2025-2026

PeT

PeT - Privacidade e Transparência

2024-2028

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

PFAI4_4eD

Programa de Formação Avançada Industria 4 - 4a edição

2023-2023

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

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

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

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
001

Laboratório

CLOUDinha

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

A framework for supporting the reproducibility of computational experiments in multiple scientific domains

Autores
Costa, L; Barbosa, S; Cunha, J;

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

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

Autores
Baccega, D; Aguilar, J; Baquero, C; Anta, AF; Ramirez, JM;

Publicação
IEEE Access

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

Distributed Generalized Linear Models: A Privacy-Preserving Approach

Autores
Tinoco, D; Menezes, R; Baquero, C;

Publicação
CoRR

Abstract

2025

CRDT-Based Game State Synchronization in Peer-to-Peer VR

Autores
Dantas, A; Baquero, C;

Publicação
Proceedings of the 12th Workshop on Principles and Practice of Consistency for Distributed Data, PaPoC 2025, World Trade Center, Rotterdam, The Netherlands, 30 March 2025- 3 April 2025

Abstract
Virtual presence demands ultra-low latency, a factor that centralized architectures, by their nature, cannot minimize. Local peer-to-peer architectures offer a compelling alternative, but also pose unique challenges in terms of network infrastructure.This paper introduces a prototype leveraging Conflict-Free Replicated Data Types (CRDTs) to enable real-time collaboration in a shared virtual environment. Using this prototype, we investigate latency, synchronization, and the challenges of decentralized coordination in dynamic non-Byzantine contexts.We aim to question prevailing assumptions about decentralized architectures and explore the practical potential of P2P in advancing virtual presence. This work challenges the constraints of mediated networks and highlights the potential of decentralized architectures to redefine collaboration and interaction in digital spaces. © 2025 Copyright is held by the owner/author(s).

Factos & Números

0Capítulos de livros

2020

16Docentes do Ensino Superior

2020

68Investigadores

2016

Contactos