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 reforça presença internacional com contribuições novas na área de sistemas de armazenamento e redes

O INESC TEC marcou presença em setembro em duas das conferências internacionais mais prestigiadas nas áreas de bases de dados e redes, a VLDB e a SIGCOMM. Os investigadores que participaram levaram ao debate internacional novas fronteiras em armazenamento, tolerância a faltas e sistemas operativos.   

29 outubro 2025

Ciência e Engenharia dos Computadores

Investigadores do INESC TEC desenvolvem novo algoritmo híbrido que melhora a fiabilidade da computação quântica

Investigadores do INESC TEC desenvolveram um novo algoritmo híbrido quântico-clássico que promete tornar a computação quântica mais prática e resiliente aos desafios dos dispositivos quânticos atuais. A investigação, intitulada “Bayesian Quantum Amplitude Estimation”, propõe uma abordagem inovadora para uma das tarefas fundamentais da computação quântica – o cálculo da amplitude, com aplicações em áreas como engenharia, finanças e inteligência artificial. 

29 outubro 2025

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

014

Projetos Selecionados

ADAPQO

Adaptive Query Optimization Architectures to Support Heterogeneous Data Intensive Applications

2025-2026

QUANTHOS

QUANTHOS - Fotónica Integrada Topológica Quântica

2025-2027

JasminCode

Developing Reliable High-performance Assembly Code using Jasmin

2025-2026

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

ATAI

Aplicação de técnicas avançadas na gestão de escalas

2025-2027

DisaggregatedHPC

Towards energy-efficient, software-managed resource disaggregation in HPC infrastructures

2025-2026

PFAI4_6eD

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

2025-2025

InfraGov

InfraGov: A Public Framework for Reliable and Secure IT Infrastructure

2025-2026

VeriFixer

VeriFixer: Automated Repair for Verification-Aware Programming Languages

2025-2026

BolsasFCT_Gestao

Financiamento Bolsas Doutoramento FCT - Gestão

2025-9999

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

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

On Quantitative Solution Iteration in QAlloy

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

Publicação
Lecture Notes in Computer Science

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. © 2025 Elsevier B.V., All rights reserved.

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
COMPUTATIONAL STATISTICS

Abstract
This paper presents a novel approach to classical linear regression, enabling accurate model computation from data streams or in a distributed setting while preserving data privacy in federated environments. We extend this framework to generalized linear models (GLMs), ensuring scalability and adaptability to diverse data distributions while maintaining privacy-preserving properties. To assess the effectiveness of our approach, we conduct numerical studies on both simulated and real datasets, comparing our method with conventional maximum likelihood estimation for GLMs using iteratively reweighted least squares. Our results demonstrate the advantages of the proposed method in distributed and federated settings.

Factos & Números

0Capítulos de livros

2020

21Investigadores Séniores

2016

1Contratados de I&D

2020

Contactos