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

    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

    INESC TEC com 5 projetos exploratórios FCT aprovados em 4 áreas de I&D

    Telecomunicações e multimédia, fotónica aplicada, software confiável e sistemas de computação avançada – são estas as quatro áreas que os investigadores do INESC TEC vão trabalhar no âmbito dos cinco projetos que foram aprovados através do Concurso de Projetos Exploratórios da Fundação para a Ciência e a Tecnologia (FCT).

    02 outubro 2024

    Ciência e Engenharia dos Computadores

    Há vantagens nas bases de dados edge — e os investigadores do INESC TEC dedicaram-se a estudá-las

    O artigo Databases in Edge and Fog Environments: A Survey, assinado por Luís Manuel Ferreira, Fábio Coelho e José Orlando Pereira e publicado na ACM Computing Surveys, estabelece conceitos inovadores na área de base de dados edge, recorrendo a diversas publicações ao nível de hardware utilizado, performance de latência, consumo de energia e privacidade. Este novo tipo de bases de dados tira partido de dispositivos situados próximos do utilizador para melhorar o desempenho e as funcionalidades oferecidas pelas mesmas.

    03 julho 2024

    Ver todas as Notícias
    002

    Projetos Selecionados

    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

    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

    2024

    Exploring Frama-C Resources by Verifying Space Software

    Autores
    Busquim e Silva, RA; Arai, NN; Burgareli, LA; Parente de Oliveira, JM; Sousa Pinto, J;

    Publicação
    Computer Science Foundations and Applied Logic

    Abstract

    2024

    Performance and explainability of feature selection-boosted tree-based classifiers for COVID-19 detection

    Autores
    Rufino, J; Ramírez, JM; Aguilar, J; Baquero, C; Champati, J; Frey, D; Lillo, RE; Fernández Anta, A;

    Publicação
    HELIYON

    Abstract
    In this paper, we evaluate the performance and analyze the explainability of machine learning models boosted by feature selection in predicting COVID-19-positive cases from self-reported information. In essence, this work describes a methodology to identify COVID-19 infections that considers the large amount of information collected by the University of Maryland Global COVID-19 Trends and Impact Survey (UMD-CTIS). More precisely, this methodology performs a feature selection stage based on the recursive feature elimination (RFE) method to reduce the number of input variables without compromising detection accuracy. A tree-based supervised machine learning model is then optimized with the selected features to detect COVID-19-active cases. In contrast to previous approaches that use a limited set of selected symptoms, the proposed approach builds the detection engine considering a broad range of features including self-reported symptoms, local community information, vaccination acceptance, and isolation measures, among others. To implement the methodology, three different supervised classifiers were used: random forests (RF), light gradient boosting (LGB), and extreme gradient boosting (XGB). Based on data collected from the UMD-CTIS, we evaluated the detection performance of the methodology for four countries (Brazil, Canada, Japan, and South Africa) and two periods (2020 and 2021). The proposed approach was assessed in terms of various quality metrics: F1-score, sensitivity, specificity, precision, receiver operating characteristic (ROC), and area under the ROC curve (AUC). This work also shows the normalized daily incidence curves obtained by the proposed approach for the four countries. Finally, we perform an explainability analysis using Shapley values and feature importance to determine the relevance of each feature and the corresponding contribution for each country and each country/year.

    FecharLer Abstract

    Factos & Números

    14Artigos em conferências indexadas

    2020

    21Investigadores Séniores

    2016

    68Investigadores

    2016

    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