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

    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

    Ciência e Engenharia dos Computadores

    A computação avançada como ponte entre Portugal e o Japão: INESC TEC e AIST reforçam cooperação científica

    Passaram cinco anos desde que o INESC TEC e o AIST - National Institute of Advanced Industrial Science and Technology -, situado no Japão, assinaram o primeiro Memorando de Entendimento (MoU). Deste acordo de cooperação científica, especialmente focado na área de computação avançada, resultaram oportunidades de intercâmbios, publicações conjuntas e troca de conhecimentos e experiências, que aproximaram os ecossistemas de I&D português e japonês – sobretudo na área de High-Performance Computing (HPC). Recentemente, os dois institutos renovaram o MoU e vão continuar a trabalhar em conjunto para potenciar a investigação em computação avançada.

    03 fevereiro 2025

    Ciência e Engenharia dos Computadores

    Há pontes a unir a engenharia biomédica e a supercomputação. Investigadoras INESC TEC voaram até Barcelona para as atravessar

    Durante uma semana, Alicia Oliveira e Beatriz Cepa trocaram os laboratórios do INESC TEC em Braga por Barcelona, onde decorreu a ACM Summer School. Ali, as investigadoras exploraram alguns dos conceitos introdutórios na área do HPC e perceberam que, num contexto dominado pela informática, a sua formação em engenharia biomédica era, afinal, uma mais-valia.

    31 outubro 2024

    Ciência e Engenharia dos Computadores

    Os bugs de software são tão persistentes como os da Natureza — uma investigação INESC TEC apertou-lhes a rede

    Investigadores INESC TEC desenvolveram a ferramenta LazyFS, capaz de injetar faltas e reproduzir bugs de perda de dados. A solução vem ajudar a compreender a origem e a causa destes bugs, mas também validar mecanismos de proteção contra as falhas. 

    07 outubro 2024

    Na era do armazenamento incessante de dados, replicá-los pode ser a chave para sistemas de grande escala. Uma investigação INESC TEC explora esses desafios

    Numa investigação publicada na revista ACM Computing Surveys, Paulo Sérgio Almeida, investigador do INESC TEC, sintetiza o conhecimento existente sobre abordagens aos Conflict-free Replicated Data Types, tópico que tem vindo a explorar na última década. Estes permitem replicação em sistemas distribuídos com resolução automática de conflitos, oferecendo grande disponibilidade — mesmo perante falhas de comunicação.

    04 outubro 2024

    Ver todas as Notícias
    004

    Projetos Selecionados

    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

    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

    Equipa
    Alcino Cunha

    Coordenador de Centro

    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

    2025

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

    Autores
    Baccega, D; Aguilar, J; Baquero, C; Fernández Anta, A; Ramirez, JM;

    Publicação

    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.

    FecharLer Abstract

    2025

    Leakage-Free Probabilistic Jasmin Programs

    Autores
    Almeida, JB; Firsov, D; Oliveira, T; Unruh, D;

    Publicação
    PROCEEDINGS OF THE 14TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2025

    Abstract
    This paper presents a semantic characterization of leakage-freeness through timing side-channels for Jasmin programs. Our characterization covers probabilistic Jasmin programs that are not constant-time. In addition, we provide a characterization in terms of probabilistic relational Hoare logic and prove the equivalence between both definitions. We also prove that our new characterizations are compositional and relate our new definitions to existing ones from prior work, which could only be applied to deterministic programs. To provide practical evidence, we use the Jasmin framework to develop a rejection sampling algorithm and provide an EasyCrypt proof that ensures the algorithm's implementation is leakage-free while not being constant-time.

    FecharLer Abstract

    2025

    Specification of paraconsistent transition systems, revisited

    Autores
    Cunha, J; Madeira, A; Barbosa, LS;

    Publicação
    SCIENCE OF COMPUTER PROGRAMMING

    Abstract
    The need for more flexible and robust models to reason about systems in the presence of conflicting information is becoming more and more relevant in different contexts. This has prompted the introduction of paraconsistent transition systems, where transitions are characterized by two pairs of weights: one representing the evidence that the transition effectively occurs and the other its absence. Such a pair of weights can express scenarios of vagueness and inconsistency. . This paper establishes a foundation for a compositional and structured specification approach of paraconsistent transition systems, framed as paraconsistent institution. . The proposed methodology follows the stepwise implementation process outlined by Sannella and Tarlecki.

    FecharLer Abstract

    2025

    Approaches to Conflict-free Replicated Data Types

    Autores
    Almeida, PS;

    Publicação
    ACM COMPUTING SURVEYS

    Abstract
    Conflict-free Replicated Data Types (CRDTs) allow optimistic replication in a principled way. Different replicas can proceed independently, being available even under network partitions and always converging deterministically: Replicas that have received the same updates will have equivalent state, even if received in different orders. After a historical tour of the evolution from sequential data types to CRDTs, we present in detail the two main approaches to CRDTs, operation-based and state-based, including two important variations, the pure operation-based and the delta-state based. Intended for prospective CRDT researchers and designers, this article provides solid coverage of the essential concepts, clarifying some misconceptions that frequently occur, but also presents some novel insights gained from considerable experience in designing both specific CRDTs and approaches to CRDTs.

    FecharLer Abstract

    2025

    Alloy Repair Hint Generation Based on Historical Data

    Autores
    Barros, A; Neto, H; Cunha, A; Macedo, N; Paiva, ACR;

    Publicação
    FORMAL METHODS, PT II, FM 2024

    Abstract
    Platforms to support novices learning to program are often accompanied by automated next-step hints that guide them towards correct solutions. Many of those approaches are data-driven, building on historical data to generate higher quality hints. Formal specifications are increasingly relevant in software engineering activities, but very little support exists to help novices while learning. Alloy is a formal specification language often used in courses on formal software development methods, and a platform-Alloy4Fun-has been proposed to support autonomous learning. While non-data-driven specification repair techniques have been proposed for Alloy that could be leveraged to generate next-step hints, no data-driven hint generation approach has been proposed so far. This paper presents the first data-driven hint generation technique for Alloy and its implementation as an extension to Alloy4Fun, being based on the data collected by that platform. This historical data is processed into graphs that capture past students' progress while solving specification challenges. Hint generation can be customized with policies that take into consideration diverse factors, such as the popularity of paths in those graphs successfully traversed by previous students. Our evaluation shows that the performance of this new technique is competitive with non-data-driven repair techniques. To assess the quality of the hints, and help select the most appropriate hint generation policy, we conducted a survey with experienced Alloy instructors.

    FecharLer Abstract

    Factos & Números

    14Artigos em conferências indexadas

    2020

    4Artigos em revistas indexadas

    2020

    16Docentes do Ensino Superior

    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