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.

    notícias
    Ciência e Engenharia dos Computadores

    INESC TEC integra consórcio ibérico para impulsionar computação quântica e inteligência artificial

    Transformar a Península Ibérica numa referência europeia em tecnologias quânticas e inteligência artificial. É este o objetivo do Quantum IberIA, um projeto de cooperação transfronteiriça que reúne 17 entidades de ambos os países, entre as quais o INESC TEC.  

    26 junho 2026

    Ciência e Engenharia dos Computadores

    Segurança dos portais de serviços públicos em teste: investigadores do INESC TEC levam resultados a vários palcos

    Da avaliação das câmaras municipais portuguesas a mais de três mil portais de serviços públicos em todo o mundo, o trabalho dos investigadores do INESC TEC Diogo Ribeiro e João Marco Silva coloca a cibersegurança da administração pública no centro do debate.   

    19 junho 2026

    Ciência e Engenharia dos Computadores

    INESC TEC com forte presença na EuroSys 2026

    De um prémio de melhor poster a contribuições em quatro frentes distintas. Foi assim que o INESC TEC marcou presença na EuroSys 2026, uma das conferências internacionais mais prestigiadas em sistemas de computação.

    15 junho 2026

    Investigador do INESC TEC integra direção de organização internacional na área de bases de dados em grafos

    Nuno Faria, investigador do INESC TEC, integra a direção do Graph Data Council (GDC), uma organização internacional sem fins lucrativos de referência na área de bases de dados em grafos. O investigador, que é também docente convidado da Escola de Engenharia da Universidade do Minho, é o único português a fazer parte da direção da GDC, da qual fazem parte membros como a Microsoft, a Oracle ou a AWS. 

    31 março 2026

    Ciência e Engenharia dos Computadores

    INESC TEC reforça projeção internacional em HPC no CENTRA 9 e consolida colaborações transnacionais

    O INESC TEC participou no CENTRA 9, encontro da rede internacional CENTRA – Collaborations to Enable Transnational Cyberinfrastructure Applications, que reúne centros de investigação, institutos e laboratórios de várias geografias para impulsionar ciberinfraestruturas transnacionais e as suas aplicações, um eixo crítico para o avanço da computação de alto desempenho e dos ecossistemas associados.    

    24 fevereiro 2026

    Ver todas as Notícias
    Tópicos
    de interesse
    Explore tópicos de interesse
    035

    Projetos em destaque

    QuantumCLP

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

    2026-2027

    POISE

    Programmable Asynchronous Asymmetric Secure Choreographies

    2026-2027

    QUANTHOS

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

    2026-2027

    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

    ADAPQO

    Adaptive Query Optimization Architectures to Support Heterogeneous Data Intensive Applications

    2025-2026

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

    ATAI

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

    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

    INSIEME

    Integrated Network for data Space and Interoperable Energy Management in Europe

    2025-2028

    InfraGov

    InfraGov: A Public Framework for Reliable and Secure IT Infrastructure

    2025-2026

    VeriFixer

    VeriFixer: Automated Repair for Verification-Aware Programming Languages

    2025-2027

    CDMS

    Claim Denial Management Solution

    2025-2026

    ENSCOMP4

    Ensino de Ciência da Computação nas Escolas 4

    2024-2026

    PeT

    PeT - Privacidade e Transparência

    2024-2028

    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

    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

    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

    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

    IDINA

    Identidade Digital Inclusiva Não Autoritativa

    2021-2025

    DigiLightRail

    Solução de Automação do Ciclo de Vida de Projectos de Sinalização Ferroviária

    2020-2023

    InterConnect

    Interoperable Solutions Connecting Smart Homes, Buildings and Grids

    2019-2024

    Equipa
    ViewClose Alphabet
    • 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.

    FecharLer Abstract

    2026

    ConflictSync: Bandwidth Efficient Synchronization of Divergent State

    Autores
    Baquero, C; Gomes, PS; Rodrigues, MB;

    Publicação
    PaPoC@EuroSys

    Abstract
    State-based Conflict-Free Replicated Data Types (CRDTs) are widely used in distributed systems to ensure high availability without coordination. However, their naive synchronization strategy, transmitting the full state, incurs high communication costs. In this paper, we: (1) propose ConflictSync, a digest-driven synchronization algorithm, which reduces total data transfer by up to 18× compared to full-state transmissions; (2) formulate state-based CRDT synchronization as set reconciliation over irredundant join decompositions; (3) generalize Rateless Set Reconciliation for variable-sized elements, at the cost of an additional communication step; (4) introduce a new generic set reconciliation solution, integrating Bloom Filters with rateless IBLTs; (5) experimentally evaluate the novel synchronization strategies. © 2026 Copyright held by the owner/author(s).

    FecharLer Abstract

    2026

    Bounding Byzantine Impact in Open CRDT Systems

    Autores
    Baquero, C; Maia, F; Dantas, A; Anta, AF; Frey, D; Sánchez, C; Albouy, T;

    Publicação
    PaPoC@EuroSys

    Abstract
    Conflict-free Replicated Data Types (CRDTs) enable available and eventually consistent data replication without coordination, making them well suited for open and partition-prone environments. Recent work has shown that CRDTs can be extended to tolerate Byzantine faults by ensuring that replicas eventually agree on the validity of operations, even in permis-sionless settings. However, validity alone does not prevent a Byzantine participant from inflicting unbounded damage by issuing large volumes of adversarial yet well-formed updates. For example, when editing text, an attacker can easily delete prior text. In this paper, we study how to bound the impact of Byzantine behavior in open CRDT systems. We introduce bounded Byzantine CRDTs, a rate-limiting framework for CRDTs in which each update carries an associated cost that limits the influence of adversarial operations relative to the resources they expend. Overall, this work bridges the gap between Byzantine-Tolerant CRDTs and resource-bounded adversarial models, providing a principled foundation for deploying CRDTs in fully open, adversarial environments. © 2026 Copyright held by the owner/author(s).

    FecharLer Abstract

    2026

    “It Makes the Code Clearer”: Why Developers Adopt ModernPython Features in Open Source Projects

    Autores
    Mendonça, W; Leite, M; Romeiro, O; Carvalho, F; Bonifácio, R; Monteiro, E; Pinto, G; Accioly, P; Saraiva, J;

    Publicação

    Abstract
    Python has become one of the most widely used programming languages, yet the transition fromPython 2 to 3 introduced a tension between innovation and compatibility. While new featuressuch as formatted string literals, type annotations, and structural pattern matching expanded thelanguage’s expressiveness, they also required substantial adaptation of legacy code. Despite theincreasing relevance of these features, there is still limited empirical evidence on how modernPython features are being adopted in practice—when developers start using them, how adoptionunfolds over time, and what motivations drive these decisions. This paper addresses this gapthrough a large-scale empirical study of 424 open-source Python projects. Our analysis revealstwo distinct adoption patterns: rapid adoption of small syntactic improvements and slowerintegration of features that require extensive refactoring or ecosystem support. On average,projects begin using with new features within 16 months after their release but take roughly 4years to achieve broader and sustained adoption. This observation may be partially explainedby the transition from Python 2 to 3, which did not preserve full backward compatibility.Complementary qualitative evidence from pull-request discussions indicates that developers areprimarily motivated to rejuvenate Python code through improvements in comprehension, safety,and performance, yet often constrained by compatibility requirements and maintenance costs.Together, these findings offer practical insights for tool developers and maintainers seeking tobalance innovation and stability in the ongoing rejuvenation of Python source code.

    FecharLer Abstract

    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
    [No abstract available]

    FecharLer Abstract