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

INESC TEC develops pioneering research in the application of variational quantum circuits to reinforcement learning

INESC TEC researchers have developed a study that aims to show the feasibility and usefulness of variational quantum circuits in terms of reinforcement learning, using quantum circuits in the central processing unit responsible for automatic decision-making. This is one of the first research papers to prove the impact of variational quantum circuits on the policy-based context, and it was recently published in the journal Quantum Machine Intelligence.  

23rd May 2023

Computer Science

INESC TEC part of European project to promote and facilitate the use of supercomputing in the European ecosystem

The EuroCC2 project started in February; the new European project by INESC TEC aims to identify and address the skills gap in high-performance computing (HPC) in the European ecosystem, and to promote cooperation across Europe, thus ensuring a consistent skills base.

27th February 2023

Computer Science

INESC TEC and UMinho analyse the impact of the Omicron variant on the efficacy of vaccination

Researchers from INESC TEC and the University of Minho analysed the impact of the Omicron variant on the effectiveness of vaccination against SARS-CoV-2 infection. The study published in the prestigious journal Scientific Reports, part of the Nature group, is the result of the work carried out by an international team within the scope of the Coronasurveys project.

01st February 2023

Computer Science

INESC TEC research improves quantum programming techniques

Recent research in quantum programming, developed by Ana Neri and José Nuno Oliveira, researchers at INESC TEC – in partnership with Rui Barbosa, Staff Researcher at the International Iberian Nanotechnology Laboratory (INL) -, proposes the concept of quantamorphisms, a recursive quantum circuit combinator that enriches quantum programming techniques.

12th January 2023

Power and Energy

INESC TEC contributes to the creation of the Energy Data Space for Europe

Over the next three years, the project ENERSHARE - European commoN EneRgy dataSpace framework enabling data sHaring-driven Across- and beyond- eneRgy sErvices-, with INESC TEC as partner, will develop a reference architecture that facilitates data sharing in the energy sector.

20th December 2022

048

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

BeFlex

Boosting engagement to increase flexibility

2022-2026

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

2023

Policy gradients using variational quantum circuits

Authors
Sequeira, A; Santos, LP; Barbosa, LS;

Publication
QUANTUM MACHINE INTELLIGENCE

Abstract
AbstractVariational quantum circuits are being used as versatile quantum machine learning models. Some empirical results exhibit an advantage in supervised and generative learning tasks. However, when applied to reinforcement learning, less is known. In this work, we considered a variational quantum circuit composed of a low-depth hardware-efficient ansatz as the parameterized policy of a reinforcement learning agent. We show that an

2023

Using survey data to estimate the impact of the omicron variant on vaccine efficacy against COVID-19 infection

Authors
Rufino, J; Baquero, C; Frey, D; Glorioso, CA; Ortega, A; Rescic, N; Roberts, JC; Lillo, RE; Menezes, R; Champati, JP; Anta, AF;

Publication
SCIENTIFIC REPORTS

Abstract
AbstractSymptoms-based detection of SARS-CoV-2 infection is not a substitute for precise diagnostic tests but can provide insight into the likely level of infection in a given population. This study uses symptoms data collected in the Global COVID-19 Trends and Impact Surveys (UMD Global CTIS), and data on variants sequencing from GISAID. This work, conducted in January of 2022 during the emergence of the Omicron variant (subvariant BA.1), aims to improve the quality of infection detection from the available symptoms and to use the resulting estimates of infection levels to assess the changes in vaccine efficacy during a change of dominant variant; from the Delta dominant to the Omicron dominant period. Our approach produced a new symptoms-based classifier, Random Forest, that was compared to a ground-truth subset of cases with known diagnostic test status. This classifier was compared with other competing classifiers and shown to exhibit an increased performance with respect to the ground-truth data. Using the Random Forest classifier, and knowing the vaccination status of the subjects, we then proceeded to analyse the evolution of vaccine efficacy towards infection during different periods, geographies and dominant variants. In South Africa, where the first significant wave of Omicron occurred, a significant reduction of vaccine efficacy is observed from August-September 2021 to December 2021. For instance, the efficacy drops from 0.81 to 0.30 for those vaccinated with 2 doses (of Pfizer/BioNTech), and from 0.51 to 0.09 for those vaccinated with one dose (of Pfizer/BioNTech or Johnson & Johnson). We also extended the study to other countries in which Omicron has been detected, comparing the situation in October 2021 (before Omicron) with that of December 2021. While the reduction measured is smaller than in South Africa, we still found, for instance, an average drop in vaccine efficacy from 0.53 to 0.45 among those vaccinated with two doses. Moreover, we found a significant negative (Pearson) correlation of around - 0.6 between the measured prevalence of Omicron in several countries and the vaccine efficacy in those same countries. This prediction, in January of 2022, of the decreased vaccine efficacy towards Omicron is in line with the subsequent increase of Omicron infections in the first half of 2022.

2023

Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications

Authors
Santo, JE; Frade, MJ; Pinto, L;

Publication
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING

Abstract
In the context of intuitionistic sequent calculus, naturality means permutation-freeness (the terminology is essentially due to Mints). We study naturality in the context of the lambda-calculus with generalized applications and its multiary extension, to cover, under the Curry-Howard correspondence, proof systems ranging from natural deduction (with and without general elimination rules) to a fragment of sequent calculus with an iterable left-introduction rule, and which can still be recognized as a call-by-name lambda-calculus. In this context, naturality consists of a certain restricted use of generalized applications. We consider the further restriction obtained by the combination of naturality with normality w.r.t. the commutative conversion engendered by generalized applications. This combination sheds light on the interpretation of naturality as a vectorization mechanism, allowing a multitude of different ways of structuring lambda-terms, and the structuring of a multitude of interesting fragments of the systems under study. We also consider a relaxation of naturality, called weak naturality: this not only brings similar structural benefits, but also suggests a new weak system of natural deduction with generalized applications which is exempt from commutative conversions. In the end, we use all of this evidence as a stepping stone to propose a computational interpretation of generalized application (whether multiary or not, and without any restriction): it includes, alongside the argument(s) for the function, a general list - a new, very general, vectorization mechanism, that structures the continuation of the computation.(c) 2022 The Author(s). Published by Elsevier Inc. This is an open access article under the CC BY-NC-ND license (http://creativecommons.org/licenses/by-nc-nd/4.0/).

2023

Privacy-Preserving Machine Learning in Life Insurance Risk Prediction

Authors
Pereira, K; Vinagre, J; Alonso, AN; Coelho, F; Carvalho, M;

Publication
MACHINE LEARNING AND PRINCIPLES AND PRACTICE OF KNOWLEDGE DISCOVERY IN DATABASES, ECML PKDD 2022, PT II

Abstract
The application of machine learning to insurance risk prediction requires learning from sensitive data. This raises multiple ethical and legal issues. One of the most relevant ones is privacy. However, privacy-preserving methods can potentially hinder the predictive potential of machine learning models. In this paper, we present preliminary experiments with life insurance data using two privacy-preserving techniques: discretization and encryption. Our objective with this work is to assess the impact of such privacy preservation techniques in the accuracy of ML models. We instantiate the problem in three general, but plausible Use Cases involving the prediction of insurance claims within a 1-year horizon. Our preliminary experiments suggest that discretization and encryption have negligible impact in the accuracy of ML models.

2023

A verified VCGen based on dynamic logic: An exercise in meta-verification with Why3

Authors
Frade, MJ; Pinto, JS;

Publication
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING

Abstract
With the incresasing importance of program verification, an issue that has been receiving more attention is the certification of verification tools, addressing the vernacular question: Who verifies the verifier?. In this paper we approach this meta-verification problem by focusing on a fundamental component of program verifiers: the Verification Conditions Generator (VCGen), responsible for producing a set of proof obligations from a program and a specification. The semantic foundations of VCGens lie in program logics, such as Hoare logic, Dynamic logic, or Separation logic, and related predicate transformers. Dynamic logic is the basis of the KeY system, one of the foremost deductive verifiers, whose logic makes use of the notion of update, which is quite intricate to formalize. In this paper we derive systematically, based on a KeY-style dynamic logic, a correct-by-construction VCGen for a toy programming language. Our workflow covers the entire process, from the logic to the VCGen. It is implemented in the Why3 tool, which is itself a program verifier. We prove the soundness and (an appropriate notion of) completeness of the logic, then define a VCGen for our language and establish its soundness. Dynamic logic is one of a variety of research topics that our dear friend and colleague Luis Soares Barbosa has, over the years, initiated and promoted at the University of Minho. It is a pleasure for us to dedicate this work to him on the occasion of his 60th birthday.

Facts & Figures

14Proceedings in indexed conferences

2020

0Book Chapters

2020

16Academic Staff

2020

Contacts