 |
VOOZH | about |
|
VOOZH | about |
At the High-Assurance Software Laboratory (HASLab), we improve practice through theory, creating and implementing software that goes beyond mere functionality: we ensure it is correct, resilient, and secure against failures and attacks.
Our team of researchers, scientists, and engineers has proven expertise in software engineering, developing methods and tools to design and integrate robust software; in distributed systems, exploring distribution and replication to ensure scalability and reliability; and in information security, addressing cybersecurity challenges and improving systems with advanced, secure cryptographic protocols, thus minimising vulnerabilities.
With a multidisciplinary approach supported by solid theoretical principles, we develop innovative solutions for critical software, secure cloud infrastructures, and privacy-aware big data management, driving scientific advancement, innovation, and high-level consultancy.
In addition, we complement our core expertise with work in human-computer interaction, programming languages, computational mathematics, and quantum computing - because we believe the future of trustworthy software is built on knowledge and innovation.
Turning the Iberian Peninsula into a European benchmark for quantum technologies and AI - that is the goal of Quantum IberIA, a cross-border cooperation project bringing together 17 entities from both countries, including INESC TEC.
26th June 2026
From assessing Portuguese municipal councils to evaluating more than 3000 public service portals worldwide, the work of INESC TEC researchers Diogo Ribeiro and João Marco Silva puts the cybersecurity of public administration at the centre of the debate.
19th June 2026
From a best poster award to contributions on four distinct fronts. That is how INESC TEC made its mark at EuroSys 2026, one of the most prestigious international conferences in computer systems.
15th June 2026
Nuno Faria, a researcher at INESC TEC, has joined the board of the Graph Data Council (GDC), a leading international non-profit organisation in the field of graph databases. Faria, who is also a guest lecturer at the School of Engineering of the University of Minho, is the only Portuguese member on the GDC board, which includes representatives from companies such as Microsoft, Oracle, and AWS.
31st March 2026
INESC TEC took part in CENTRA 9, a meeting of the international CENTRA (Collaborations to Enable Transnational Cyberinfrastructure Applications) network, which brings together research centres, institutes and laboratories from various regions to advance transnational cyberinfrastructures and their applications – a critical pillar for the progress of high-performance computing (HPC) and associated ecosystems.
24th February 2026
Open Design Ecosystem for European Chips - Productivity, Interoperability, Verification
2026-2029
Boosting the Immunity of Storage Systems Against Ransomware
2026-2029
Manipulador Móvel Inteligente com Programação Intuitiva e Controlo Agnóstico
2026-2029
National Competence Centres in the framework of EuroHPC Phase 3
2026-2029
Quantum computing optimization for container loading problems: a new frontier in logistics optimization
2026-2027
Programmable Asynchronous Asymmetric Secure Choreographies
2026-2027
QUANTHOS - Fotónica Integrada Topológica Quântica
2026-2027
Cibersegurança e Recuperação de Dados Inteligente e Auto-Configurável para a Resiliência contra Ransomware
2026-2029
EuroHPC traineeships in Hosting Entities, Centres of Excellence and Competence Centres, SMEs and Industry
2026-2029
QUANTUM IBER_IA: Impulso estratégico de las capacidades en tecnologías cuánticas e inteligencia artificial en el espacio ibérico transfronterizo
2026-2028
Adaptive Query Optimization Architectures to Support Heterogeneous Data Intensive Applications
2025-2026
A paraconsistent inference engine to support research in age-ralated molecular degeneration
2025-2028
Developing Reliable High-performance Assembly Code using Jasmin
2025-2026
Piloto de Robótica Móvel e Cibersegurança em Ambientes Industriais sobre Comunicações 5G – Europneumaq
2025-2026
Aplicação de técnicas avançadas na gestão de escalas
2025-2026
Strengthening CI/CD Pipeline Cybersecurity and Safeguarding the Intellectual Property
2025-2028
SafeIaC: Reliable Analysis and Automated Repair for Infrastructure as Code
2025-2028
Programa de Formação Avançada Industria 4 - 6a edição
2025-2025
Integrated Network for data Space and Interoperable Energy Management in Europe
2025-2028
Towards energy-efficient, software-managed resource disaggregation in HPC infrastructures
2025-2026
InfraGov: A Public Framework for Reliable and Secure IT Infrastructure
2025-2026
VeriFixer: Automated Repair for Verification-Aware Programming Languages
2025-2027
JRC Interoperability Laboratory Adoption of the Semantic Interoperability Framework
2025-2025
Claim Denial Management Solution
2025-2026
Funding FCT PhD Grants - Management
2025-9999
Ensino de Ciência da Computação nas Escolas 4
2024-2026
PeT - Privacidade e Transparência
2024-2028
Programa de Formação Avançada Industria 4 - 5a edição
2024-2024
exaSIMPLE: A Hybrid ML-CFD SIMPLE Algorithm for the Exascale Era
2024-2025
High-level specialised application support service in High-Performance Computing (HPC)
2024-2028
BCD.S+M - Modular Blockchain Data Storage and Management System with AI
2024-2027
Digital Twin for Europe
2024-2026
Holistic Approach towards Empowerment of the DiGitalization of the Energy Ecosystem through adoption of IoT solutions
2024-2027
Hpc AlliaNce for Applications and supercoMputing Innovation: the Europe - Japan collaboration
2024-2027
Programa de Formação Avançada Industria 4 - 4a edição
2023-2023
QuantELM: from Ultrafast optical processors to Quantum Extreme Learning Machines with integrated optics
2023-2024
Alliance for Energy Transition
2023-2026
Energy-efficient AI-ready Data Spaces
2023-2025
National Competence Centres in the framework of EuroHPC Phase 2
2023-2026
Deteção de atividade no interior do veículo
2022-2023
Digital Innovation Hub for Artificial Intelligence and High-Performance Computing
2022-2026
Agenda New Space Portugal
2022-2026
Boosting engagement to increase flexibility
2022-2026
European commoN EneRgy dataSpace framework enabling data sHaring-driven Across- and beyond- eneRgy sErvices
2022-2025
Parecer sobre a implementação de software para redes elétricas inteligentes
2022-2022
Programa de Formação Avançada Industria 4 - 3a edição
2022-2022
Automated Perception Driving
2022-2023
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
Constraint-based Specification Repair
2022-2023
Towards Energy-aware Communications: Connecting the power grid and communication infrastructure
2022-2023
Identidade Digital Inclusiva Não Autoritativa
2021-2025
Computação de elevado desempenho sustentável
2021-2025
Building the Digital Thread for Circular Economy Product, Resource & Service Management
2021-2025
Exploring the Impact of Formal Verification on the Adoption of Password Security Software
2021-2022
Análise de Requisitos e Especificação Funcional de uma Arquitetura Distribuída baseada em soluções IoT para a Gestão e Controlo da Rede de Distribuição
2021-2023
A network for supporting the coordination of High-Performance Computing research between Europe and Latin America
2021-2023
Solução de Automação do Ciclo de Vida de Projectos de Sinalização Ferroviária
2020-2023
Programa de Formação Avançada Industria 4.0
2020-2021
Programmable and Adaptable Storage for AI-oriented HPC Ecosystems
2020-2021
Automating Crash-Consistency Testing for Persistent Memory
2020-2021
Adaptive, Intelligent and Distributed Assurance Platform
2020-2023
A Management Framework for Consolidated Big Data and HPC
2020-2023
Prestação de Serviços no ambito do projeto SKORR
2020-2021
Interoperable Solutions Connecting Smart Homes, Buildings and Grids
2019-2024
Training 4 Cotec, Digital Transformation Knowledge Challenge - Elaboração de Programa de Formação “CONHECER E COMPREENDER O DESAFIO DAS TECNOLOGIAS DE TRANSFORMAÇÃO DIGITAL”
2019-2021
Cloud for CANDY
2019-2019
HArdware-backed trusted and scalable DEcentralized Systems
2018-2022
Aprendizagem Automática para Deteção de Ataques e Identificação de Perfis Segurança na Internet
2018-2022
Advancing the Frontier of Social Media Management Tools
2018-2021
Distributed architectures: variability and interaction for cyber-physical systems
2018-2022
Safery verification for robotic software
2018-2021
Coalgebraic modeling and analysis for computational synthetic biology
2018-2021
Demonstration of INTElligent grid technologies for renewables INTEgration and INTEractive consumer participation enabling INTEroperable market solutions and INTErconnected stakeholders
2017-2020
Lightweight Computation for Networks at the Edge
2017-2019
European Cloud In-Memory Database Appliance with Predictable Performance for Critical Applications
2016-2019
PLATAFORMA DE PREPARAÇÃO DE CONTEÚDOS AUDIOVISUAIS PARA INGEST NA CLOUD
2016-2019
GreenSoftwareLab: Towards an Engineering Discipline for Green Software
2016-2019
CORAL – Sustainable Ocean Exploitation: Tools and Sensors
2016-2018
Secure and Resilient Cloud Architecture
2015-2018
NanoSTIMA - Macro-to-Nano Human Sensing Technologies
2015-2019
NanoSTIMA - Health data infrastructure
2015-2019
SMILES - Smart, Mobile, Intelligent and Large scale Sensing and analytics
2015-2019
Real proven solutions to enable active demand and distributed generation flexible integration, through a fully controllable LOW Voltage and medium voltage distribution grid
2015-2017
Ultra-Scalable and Ultra-Efficient Integrated and Visual Big Data Analytics
2014-2017
Privacy-Preserving Computation in the Cloud
2013-2016
A Coherent and Rich PaaS with a Common Programming Model
2013-2016
Research Assistant
External Research Collaborator
Research Assistant
Centre Coordinator
Senior Researcher
Research Assistant
External Student
Senior Researcher
Research Assistant
External Student
Research Assistant
Advisor to the Centre Coordinator
External Administrative and Technical Staff
Assistant Researcher
Research Assistant
External Student
Research Assistant
External Student
Research Assistant
External Student
External Research Collaborator
Research Assistant
External Student
External Student
External Student
External Student
Senior Researcher
External Student
External Research Collaborator
External Research Collaborator
External Research Collaborator
External Research Collaborator
Research Assistant
Research Assistant
External Student
External Student
Research Assistant
External Student
Research Assistant
External Student
Research Assistant
Senior Researcher
External Research Collaborator
Research Coordinator
Senior Researcher
Senior Researcher
Research Coordinator
External Student
External Student
External Research Collaborator
External Research Collaborator
Research Coordinator
Research Coordinator
External Research Collaborator
Research Assistant
Research Assistant
Research Assistant
External Research Collaborator
External Research Collaborator
External Research Collaborator
External Student
External Student
Research Assistant
Senior Researcher
Senior Researcher
Research Assistant
External Student
Technical Specialist
External Research Collaborator
External Research Collaborator
Research Assistant
External Research Collaborator
External Research Collaborator
Research Assistant
External Research Collaborator
External Research Collaborator
External Research Collaborator
Diretor
Research Assistant
External Research Collaborator
HASLab Publications
2026
Authors
Lourenço, CB; Pinto, JS;
Publication
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.
2026
Authors
Baquero, C; Gomes, PS; Rodrigues, MB;
Publication
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).
2026
Authors
Baquero, C; Maia, F; Dantas, A; Anta, AF; Frey, D; Sánchez, C; Albouy, T;
Publication
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).
2026
Authors
Mendonça, W; Leite, M; Romeiro, O; Carvalho, F; Bonifácio, R; Monteiro, E; Pinto, G; Accioly, P; Saraiva, J;
Publication
Abstract
2026
Authors
Alves, T; Campos, JC; Chalmers, A;
Publication
COMPUTERS & GRAPHICS-UK
Abstract
[No abstract available]
The access to the final selection minute is only available to applicants.
Please check the confirmation e-mail of your application to obtain the access code.
