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 cooperação UE–Brasil em supercomputação e tecnologias quânticas

    O INESC TEC participou no workshop internacional “Identifying potential core areas of HPC cooperation between the EU and Brazil”, no Laboratório Nacional de Computação Científica (LNCC), em Petrópolis, Brasil. O evento, organizado pelo Ministério Brasileiro da Ciência, Tecnologia e Inovação (MCTI) e pela Delegação da União Europeia no Brasil, reuniu investigadores, decisores políticos e científicos e representantes da indústria para identificar áreas estratégicas de cooperação entre a União Europeia e o Brasil no domínio da computação de alto desempenho (HPC) e das tecnologias quânticas. 

    21 janeiro 2026

    Ciência e Engenharia dos Computadores

    Projeto BANKSY arranca para revolucionar o raciocínio sobre informação vaga e contraditória

    O projeto BANKSY, financiado pela FCT, promete inovar o modo como lidamos com contextos marcados por informações incompletas, incertas ou até contraditórias. Com duração prevista de três anos, o projeto resulta de uma parceria entre o INESC TEC, o CIDMA, a Universidade de Aveiro e a AIBILI (Association for Innovation and Biomedical Research on Light and Image).

    16 dezembro 2025

    INESC TEC e Carnegie Mellon University unem forças para criar a próxima geração de otimizadores de bases de dados

    Numa altura em que a complexidade e popularidade das aplicações baseadas em dados cresce a um ritmo sem precedentes, o INESC TEC e a Carnegie Mellon University (CMU) estão a colaborar num projeto para atacar um dos problemas mais discutidos na área: a eficiência dos sistemas de processamento de dados que as suportam. O projeto chama-se ADAPQO e pretende transformar a forma como as bases de dados tomam decisões.

    11 dezembro 2025

    Ciência e Engenharia dos Computadores

    “Quien sabe por Algebra, sabe scientificamente” – a jubilação de José Nuno Oliveira marca uma era na informática da UMinho

    Mais de quatro décadas passaram desde o primeiro dia de José Nuno Oliveira na Universidade do Minho (UMinho). No dia 14 de novembro, o Auditório A1 do Campus de Gualtar da Universidade do Minho (UMinho), em Braga, foi palco de uma despedida que mexeu com sentimentos e memórias. A comunidade da UMinho, e não só, reuniu-se para celebrar a dedicação de José Nuno Oliveira ao ensino, à investigação e à formação de gerações em Engenharia Informática. 

    28 novembro 2025

    INESC TEC projeta supercomputação nacional para a linha da frente europeia

    O INESC TEC voltou a marcar presença no centro das decisões europeias, desta vez, na área da supercomputação. A Vice-Presidente Executiva da Comissão Europeia, Henna Virkkunen, visitou, no dia 10 de novembro, o supercomputador Deucalion, instalado na Universidade do Minho (UMinho) em Guimarães, numa visita que destacou o contributo português para a estratégia digital e científica da União Europeia na área.   

    27 novembro 2025

    Ver todas as Notícias
    004

    Projetos Selecionados

    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

    QuantumCLP

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

    2025-2027

    BigHPC

    2020-2023

    Equipa
    Alcino Cunha

    Investigador Coordenador

    António Luís Sousa

    Coordenador de Centro

    Catarina Leones Fernandes

    Adjunto da Coordenação de Centro

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

    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

    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.

    FecharLer Abstract

    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.

    FecharLer Abstract

    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.

    FecharLer Abstract

    Factos & Números

    21Investigadores Séniores

    2016

    68Investigadores

    2016

    4Artigos em revistas indexadas

    2020

    Ver todos os Factos & Números
    Contactos
    António Luís Sousa

    -

    +351253604440

    antonio.l.sousa@inesctec.pt

    Alcino Cunha

    Coordenado de Centro

    +351253604440

    alcino.cunha@inesctec.pt