Cookies Policy
The website need some cookies and similar means to function. If you permit us, we will use those means to collect data on your visits for aggregated statistics to improve our service. Find out More
Accept Reject
  • Menu
    Facts & Numbers
    000
    Presentation

    High-Assurance Software

    HASLab is focused on the design and implementation of high-assurance software systems: software that is correct by design and resilient to environment faults and malicious attacks. 

    To accomplish this mission, HASLab covers three main competences — Cybersecurity, Distributed Systems, and Software Engineering — complemented by other competences such as Human-Computer Interaction, Programming Languages, or the Mathematics of Computing. 

    Software Engineering – methods, techniques, and tools for rigorous software development, that can be applied to the internal functionality of a component, its composition with other components, as well as the interaction with the user.

    Distributed Systems – improving the reliability and scalability of software, by exploring properties inherent to the distribution and replication of computer systems.

    Cybersecurity – minimize the vulnerability of software components to hostile attacks, by deploying structures and cryptographic protocols whose security properties are formally proven.

    Through a multidisciplinary approach that is based on solid theoretical foundations, we aim to provide solutions — theory, methods, languages, tools — for the development of complete ICT systems that provide strong guarantees to their owners and users. Prominent application areas of HASLab research include the development of safety and security critical software systems, the operation of secure cloud infrastructures, and the privacy-preserving management and processing of big data.

    Latest News
    Computer Science and Engineering

    There are bridges uniting biomedical engineering and supercomputing - INESC TEC researchers flew to Barcelona to cross them

    For a week, Alicia Oliveira and Beatriz Cepa left INESC TEC's laboratories in Braga and went to Barcelona - the city that welcomed the ACM Summer School. The researchers explored some of the elemental HPC concepts and realised that - in a context dominated by computer science - their training in biomedical engineering was an asset.

    31st October 2024

    Computer Science and Engineering

    Software bugs are as persistent as those in nature - a study by INESC TEC closed in on them

    INESC TEC researchers developed the LazyFS tool, capable of injecting faults and reproducing data loss bugs. The solution helps to understand the origin and cause of said bugs, but also to validate protection mechanisms against failures. 

    07th October 2024

    In the era of pervading data storage, replication can be the key to large-scale systems. Here’s how a INESC TEC research explores these challenges

    In a study published in ACM Computing Surveys, Paulo Sérgio Almeida, INESC TEC researcher, synthesises the existing knowledge on approaches to Conflict-free Replicated Data Types, a topic he has been exploring over the past decade. These enable replication in distributed systems with automatic conflict resolution, ensuring high availability – even in the face of communication failures.

    04th October 2024

    INESC TEC with five FCT exploratory projects approved in four R&D areas

    Telecommunications and Multimedia, Applied Photonics, High-assurance Software and Advanced Computing Systems – these are the four domains that INESC TEC researchers will explore within the scope of the five projects that were approved through the Call for Exploratory Projects promoted by the Foundation for Science and Technology (FCT).

    02nd October 2024

    Computer Science and Engineering

    Edge databases have many benefits — and INESC TEC researchers have dedicated themselves to studying them

    The paper Databases in Edge and Fog Environments: A Survey, signed by Luís Manuel Ferreira, Fábio Coelho and José Orlando Pereira - and published in ACM Computing Surveys -, establishes innovative concepts in the edge databases area, resorting to several publications on hardware used, latency performance, energy consumption and privacy. This new type of database benefits from devices close to the users to improve performance and features.

    03rd July 2024

    View all News
    001

    Projects

    BCDSM

    BCD.S+M - Modular Blockchain Data Storage and Management System with AI

    2024-2027

    Team
    Alcino Cunha

    Centre Coordinator

    António Luís Sousa

    Centre Coordinator

    Catarina Leones Fernandes

    Advisor to the Centre Coordinator

    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

    Laboratory

    CLOUDinha

    Publications

    HASLab Publications

    View all Publications

    2025

    Specification of paraconsistent transition systems, revisited

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

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

    CloseRead Abstract

    2025

    Approaches to Conflict-free Replicated Data Types

    Authors
    Almeida, PS;

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

    CloseRead Abstract

    2025

    Alloy Repair Hint Generation Based on Historical Data

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

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

    CloseRead Abstract

    2024

    Exploring Frama-C Resources by Verifying Space Software

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

    Publication
    Computer Science Foundations and Applied Logic

    Abstract

    2024

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

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

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

    CloseRead Abstract

    Facts & Figures

    4Papers in indexed journals

    2020

    0Book Chapters

    2020

    1R&D Employees

    2020

    View all Facts & Figures
    Contacts
    António Luís Sousa

    Centre Coordinator

    +351253604440

    antonio.l.sousa@inesctec.pt

    Alcino Cunha

    Centre Coordinator

    +351253604440

    alcino.cunha@inesctec.pt