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
Informática

INESC TEC desenvolve investigação pioneira na aplicação de circuitos variacionais quânticos à aprendizagem de reforço

Investigadores do INESC TEC desenvolveram um estudo que visa mostrar a viabilidade e utilidade dos circuitos variacionais quânticos no domínio da aprendizagem por reforço, através da utilização de circuitos quânticos na unidade de processamento central responsável pela tomada de decisão automática. Trata-se de um dos primeiros trabalhos de investigação a provar o impacto dos circuitos variacionais quânticos no contexto “policy-based” e foi recentemente publicado na revista Quantum Machine Intelligence.

23 maio 2023

Informática

INESC TEC participa em projeto europeu para promover e facilitar o uso de supercomputação no ecossistema europeu

O projeto EuroCC2 arrancou em fevereiro e é o novo projeto europeu do INESC TEC que pretende, por um lado, identificar e colmatar as lacunas em termos de competências em computação de alto desempenho (HPC) no ecossistema europeu e, por outro, promover a cooperação em toda a Europa para assegurar uma base de competências consistente.

27 fevereiro 2023

Informática

INESC TEC e UMinho analisam impacto da variante Ómicron na eficácia da vacinação

Investigadores do INESC TEC e da Universidade do Minho analisaram o impacto da variante Ómicron na eficácia da proteção conferida pela vacinação contra a infeção pelo vírus SARS-CoV-2. O estudo publicado na conceituada revista Scientific Reports, do grupo Nature, é resultado do trabalho de uma equipa internacional, no âmbito do projeto Coronasurveys.

01 fevereiro 2023

Informática

Investigação INESC TEC melhora técnicas de programação quântica

Investigação recente na área da programação quântica, desenvolvida por Ana Neri e José Nuno Oliveira, investigadores do INESC TEC, em colaboração com Rui Barbosa, Staff Researcher no Laboratório Ibérico Internacional de Nanotecnologia (INL), propõe o conceito de quantamorfismo, um combinador recursivo de circuitos quânticos que enriquece as técnicas de programação quântica.

12 janeiro 2023

Energia

INESC TEC contribui para a criação do Espaço Europeu de Dados Energéticos

Ao longo dos próximos três anos, o projeto ENERSHARE - European commoN EneRgy dataSpace framework enabling data sHaring-driven Across- and beyond- eneRgy sErvices-, do qual o INESC TEC é parceiro, pretende desenvolver uma arquitetura de referência que facilite a partilha de dados no setor energético.

20 dezembro 2022

048

Projetos Selecionados

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

Investigação do Impacto de Verificação Formal na Adopção de Software para Segurança de Passwords

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

Sistemas descentralizados confiáveis e escaláveis suportados por hardware

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

Architecturas distribuídas: variabilidade e interação de sistemas ciber-físicos

2018-2022

SAFER

Verificação de segurança para software robótico

2018-2021

KLEE

Modelação coalgébrica e análise para biologia sintética computacional

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: Computação Verde como uma Disciplina de Engenharia

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

TEC4Growth - RL 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

Análise Integrada e Visual de Big Data Ultra-escalável e Ultra-eficiente

2014-2017

Practice

Ferramentas de Preservação de Privacidade na Cloud

2013-2016

CoherentPaaS

PaaS Rica e Coerente com um Modelo de Programação Comum

2013-2016

Equipa
001

Laboratório

CLOUDinha

Publicações

HASLab Publicações

Ler todas as publicações

2023

Policy gradients using variational quantum circuits

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

Publicação
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

Autores
Rufino, J; Baquero, C; Frey, D; Glorioso, CA; Ortega, A; rešcic, N; Roberts, JC; Lillo, RE; Menezes, R; Champati, JP; Fernández Anta, A;

Publicação
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

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

Publicação
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

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

Publicação
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

Autores
Frade, MJ; Pinto, JS;

Publicação
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.

Factos & Números

21Investigadores Séniores

2016

1Contratados de I&D

2020

16Docentes do Ensino Superior

2020

Contactos