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

Portuguese Institute part of project to improve the flexibility of the European energy system

Over the next four years, the BeFlexible - Boosting Engagement to Increase Flexibility project will increase the flexibility of the energy system, improve cooperation between Distribution System Operators (DSOs) and Transmission System Operators (TSOs), and facilitate communication between all energy stakeholders. The Institute for Systems and Computer Engineering, Technology and Science (INESC TEC) is the only Portuguese partner of the project, which will be financed by the European Commission (€10M) through the Horizon Europe programme.

06th December 2022

Researcher explores the versatility of partitioned Bloom Filters in the design of data structures

The study by Paulo Sérgio Almeida, INESC TEC researcher and professor at the University of Minho, focuses on Bloom Filters, a very popular probabilistic data structure in the design of databases, distributed systems, and communication networks. The study, which demonstrates the versatility of partitioned Bloom Filters, was accepted for publication in IEEE Transactions on Computers, one of the top journals in Informatics and Computing.

29th November 2022

INESC TEC research on Alloy specification language presented at top software engineering conference

A team of INESC TEC researchers working on the Alloy language and specification tool presented the QAlloy extension at the ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), a top conference in the area of software engineering that took place between November 14 and 18, in Singapore.

22nd November 2022

RISC2 project acknowledged by international journal specialised in advanced computing

The RISC2 project, which aims to promote and improve the relationship between research and innovation communities in Europe and Latin America, won the HPCwire Editor’s Choice Awards in the category of Best HPC Collaboration.

21st November 2022

INESC TEC welcomed students at the “Verão no Campus” in Braga

Close to 20 high school students visited INESC TEC’s High-assurance Software Laboratory (HASLab). The visit took place within the scope of the “Computação sem Fronteiras” initiative, one of several activities part of the “Verão no Campus” – promoted by the University of Minho; the activities took place between July 18 and 22, in the Department of Informatics (DI) of the University of Minho, Braga.  

28th July 2022

047

Projects

fMP

Formação de Introdução à utilização de recursos HPC (Técnicas básicas de Programação Paralela)

2022-2022

AURORA

Deteção de atividade no interior do veículo

2022-2024

NewSpacePortugal

Agenda New Space Portugal

2022-2025

ENERSHARE

European commoN EneRgy dataSpace framework enabling data sHaring-driven Across- and beyond- eneRgy sErvices

2022-2025

Gridsoft

Parecer sobre a implementação de software para redes elétricas inteligentes

2022-2022

PFAI4_3ed

Programa de Formação Avançada Industria 4 - 3a edição

2022-2022

THEIA

Automated Perception Driving

2022-2023

SpecRep

Constraint-based Specification Repair

2022-2023

IBEX

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

FLEXCOMM

Towards Energy-aware Communications: Connecting the power grid and communication infrastructure

2022-2023

ATE

Alliance for Energy Transition

2022-2025

Sustainable HPC

Computação de elevado desempenho sustentável

2021-2023

CircThread

Building the Digital Thread for Circular Economy Product, Resource & Service Management

2021-2025

PassCert

Exploring the Impact of Formal Verification on the Adoption of Password Security Software

2021-2022

IoT4Distribuicao

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

RISC2

A network for supporting the coordination of High-Performance Computing research between Europe and Latin America

2021-2023

CloudAnalytics4Dams

Gestão de Grandes Quantidades de Dados em Barragens da EDP Produção

2021-2021

PAStor

Programmable and Adaptable Storage for AI-oriented HPC Ecosystems

2020-2021

PFAI4.0

Programa de Formação Avançada Industria 4.0

2020-2021

Collaboration

Collaborative Visual Development

2020-2021

AIDA

Adaptive, Intelligent and Distributed Assurance Platform

2020-2023

BigHPC

A Management Framework for Consolidated Big Data and HPC

2020-2023

SLSNA

Prestação de Serviços no ambito do projeto SKORR

2020-2021

AppOwl

Deteção de Mutações Maliciosas no Browser

2020-2021

InterConnect

Interoperable Solutions Connecting Smart Homes, Buildings and Grids

2019-2024

T4CDTKC

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

CLOUD4CANDY

Cloud for CANDY

2019-2019

HADES

HArdware-backed trusted and scalable DEcentralized Systems

2018-2022

MaLPIS

Aprendizagem Automática para Deteção de Ataques e Identificação de Perfis Segurança na Internet

2018-2022

SKORR

Advancing the Frontier of Social Media Management Tools

2018-2021

DaVinci

Distributed architectures: variability and interaction for cyber-physical systems

2018-2022

SAFER

Safery verification for robotic software

2018-2021

KLEE

Coalgebraic modeling and analysis for computational synthetic biology

2018-2021

InteGrid

Demonstration of INTElligent grid technologies for renewables INTEgration and INTEractive consumer participation enabling INTEroperable market solutions and INTErconnected stakeholders

2017-2020

Lightkone

Lightweight Computation for Networks at the Edge

2017-2019

CloudDBAppliance

European Cloud In-Memory Database Appliance with Predictable Performance for Critical Applications

2016-2019

GSL

GreenSoftwareLab: Towards an Engineering Discipline for Green Software

2016-2019

Cloud-Setup

PLATAFORMA DE PREPARAÇÃO DE CONTEÚDOS AUDIOVISUAIS PARA INGEST NA CLOUD

2016-2019

CORAL-TOOLS

CORAL – Sustainable Ocean Exploitation: Tools and Sensors

2016-2018

SafeCloud

Secure and Resilient Cloud Architecture

2015-2018

NanoStima-RL1

NanoSTIMA - Macro-to-Nano Human Sensing Technologies

2015-2019

NanoStima-RL3

NanoSTIMA - Health data infrastructure

2015-2019

SMILES

SMILES - Smart, Mobile, Intelligent and Large scale Sensing and analytics

2015-2019

UPGRID

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

LeanBigData

Ultra-Scalable and Ultra-Efficient Integrated and Visual Big Data Analytics

2014-2017

Practice

Privacy-Preserving Computation in the Cloud

2013-2016

CoherentPaaS

A Coherent and Rich PaaS with a Common Programming Model

2013-2016

Team
001

Laboratory

CLOUDinha

Publications

HASLab Publications

View all Publications

2022

Compiling Quantamorphisms for the IBM Q Experience

Authors
Neri, A; Barbosa, RS; Oliveira, JN;

Publication
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING

Abstract
Based on the connection between the categorical derivation of classical programs from specifications and a category-theoretic approach to quantum information, this paper contributes to extending the laws of classical program algebra to quantum programming. This aims at building correct-by-construction quantum circuits to be deployed on quantum devices such as those available through the IBM Q Experience. Reversibility is ensured by minimal complements. Such complementation is extended inductively to encompass catamorphisms on lists (vulgo folds), giving rise to the corresponding recursion scheme in reversible computation. The same idea is then applied to the setting of quantum programming, where computation is expressed by unitary transformations. This yields the notion of 'quantamorphism', a structural form of quantum recursion implementing cycles and folds on lists with quantum control flow. By Kleisli correspondence, quantamorphisms can be written as monadic functional programs with quantum parameters. This enables the use of Haskell, a monadic functional programming language, to perform the experimental work. Such calculated quantum programs prepared in Haskell are pushed through Quipper and the Qiskit interface to IBM Q quantum devices. The generated quantum circuits - often quite large - exhibit the predicted behaviour. However, running them on real quantum devices naturally incurs a significant amount of errors. As quantum technology is rapidly evolving, an increase in reliability is likely in the future, allowing for our programs to run more accurately.

2022

Cross-domain Modelling of Verification and Validation Workflows in the Large Scale European Research Project VALU3S Invited Paper

Authors
Bauer, T; Agirre, JA; Furcho, D; Herzner, W; Hruska, B; Karaca, M; Pereira, D; Proenca, J; Schlick, R; Sicher, R; Smrcka, A; Yayan, U; Sangchoolie, B;

Publication
EMBEDDED COMPUTER SYSTEMS: ARCHITECTURES, MODELING, AND SIMULATION, SAMOS 2021

Abstract
The complexity of systems continues to increase rapidly, especially due to the multi-level integration of subsystems from different domains into cyber-physical systems. This results in special challenges for the efficient verification and validation (V&V) of these systems with regard to their requirements and properties. In order to tackle the new challenges and improve the quality assurance processes, the V&V workflows have to be documented and analyzed. In this paper, a novel approach for the workflow modelling of V&V activities is presented. The generic approach is tailorable to different industrial domains and their specific constraints, V&V methods, and toolchains. The outcomes comprise a dedicated modelling notation (VVML) and tool-support using the modelling framework Enterprise Architect for the efficient documentation and implementation of workflows in the use cases. The solution enables the design of re-usable workflow assets such as V&V activities and artifacts that are exchanged between workflows. This work is part of the large scale European research project VALU3S that deals with the improvement and evaluation of V&V processes in different technical domains, focusing on safety, cybersecurity, and privacy properties.

2022

Graded epistemic logic with public announcement

Authors
Benevides, M; Madeira, A; Martins, MA;

Publication
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING

Abstract
This work introduces a new fuzzy epistemic logic with public announcement with fuzzyness on both transitions and propositions. The interpretation of the connectives is done over the Godel algebra and the interpretation of public announcements in this logic generalises the traditional update one. The core idea is that, the effect of a public announcement is reflected on the transitions degrees of the models. The update takes in account not only the truth degree of the announcement, at a target state, but also the degree of the transitions reaching that state. We prove the soundness of all axioms of the multi-agent epistemic logic with public announcements with respect to this graded semantics. Finally, we introduce the notion of bisimulation and prove the modal invariance property for our logic.

2022

Boolean Searchable Symmetric Encryption with Filters on Trusted Hardware

Authors
Ferreira, B; Portela, B; Oliveira, T; Borges, G; Domingos, H; Leitao, J;

Publication
IEEE TRANSACTIONS ON DEPENDABLE AND SECURE COMPUTING

Abstract

2022

Timely Specification Repair for Alloy 6

Authors
Cerqueira, J; Cunha, A; Macedo, N;

Publication
SOFTWARE ENGINEERING AND FORMAL METHODS, SEFM 2022

Abstract

Supervised Theses

2021

The Role of Business and Innovation Strategies in Company Competittive Performance in an Uncertain Context

Author
Sofia Pinto Simões Figueira Canada

Institution
UP-FEP

2021

Otimização da exploração de redes de distribuição com integração de centrais elétricas virtuais

Author
Joana Moura Pereira Duro

Institution
UTAD

2021

Momentos da Verdade no serviço funerário

Author
Gustavo Gomes de Barros Melro Craveiro

Institution
UP-FEP

2021

Exposição aos campos eletromagnéticos em ressonância magnética: implementação de boas práticas

Author
Vítor Manuel da Fonseca e Silva

Institution
UP-FEUP

2021

Organização, Classificação e Análise de Reviews Online Direcionadas ao Retalho do Município do Porto

Author
Pedro Miguel Baldaia Braga da Costa

Institution
UP-FEP

Facts & Figures

4Papers in indexed journals

2020

0Book Chapters

2020

14Proceedings in indexed conferences

2020

Contacts