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

INESC TEC developed an application for managing large databases in real time

Nowadays, database management and updating is a key concern for large companies. In order to perform said critical tasks, the purchase of dedicated hardware is the solution found by most organisations; however, this leads to expenses in terms of hardware management and maintenance, and often the need to allocate human resources. Now, there’s a cloud platform that aims to meet the market demands, with a more reliable and cost-effective technology that can be updated in real time.

11th January 2020

HASLab welcomes students from the 2019 Best Student programme at University of Minho

On December 19th, INESC TEC’s High-Assurance Software Laboratory (HASLab) welcomed six students from Braga, Guimarães, Santo Tirso and Terras de Bouro, who chose HASLab to discover and become familiar with the work of a researcher in the IT field. This event was part of the 2019 edition of the Best Student programme at UMinho.

07th January 2020

Last lesson of José Manuel Valença with a full house

José Manuel Valença, researcher of INESC TEC’s High-Assurance Software Laboratory (HASLab) and Full Professor at the School of Engineering of the University of Minho, lectured his last lesson on 18 October at the University of Minho in Braga.

13th November 2019

INESC TEC participates in an international conference on the reliable distributed systems area

A team of researchers of INESC TEC’s High-Assurance Software Laboratory (HASLab) participated at the 38th International Symposium on Reliable Distributed Systems (SRDS 2019), which took place in Lyon, France, from 1 to 4 October, presenting four scientific papers and organising a workshop, among other tasks.

13th November 2019

INESC TEC organises world congress with 600 professionals in the computer science field

The FM’19 – 3rd World Congress on Formal Methods, an event that gathers the worldwide computer experts, took place in Porto between 7 and 11 October.

31st October 2019

060

Projects

exaSIMPLE

exaSIMPLE: A Hybrid ML-CFD SIMPLE Algorithm for the Exascale Era

2024-2025

Saude24GB

Linha de Saúde 24h da Guiné-Bissau

2024-2024

EPICURE

High-level specialised application support service in High-Performance Computing (HPC)

2024-2028

TwinEU

Digital Twin for Europe

2024-2026

HANAMI

Hpc AlliaNce for Applications and supercoMputing Innovation: the Europe - Japan collaboration

2024-2026

ENSCOMP3

Ensino de Ciência da Computação nas Escolas 3

2023-2025

AzDIH

Azores Digital Innovation Hub on Tourism and Sustainability

2023-2025

PFAI4_4eD

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

2023-2023

ATE

Alliance for Energy Transition

2023-2025

Green_Dat_AI

Energy-efficient AI-ready Data Spaces

2023-2025

EuroCC2

National Competence Centres in the framework of EuroHPC Phase 2

2023-2025

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

NewSpacePortugal

Agenda New Space Portugal

2022-2025

ATTRACT_DIH

Digital Innovation Hub for Artificial Intelligence and High-Performance Computing

2022-2025

BeFlexible

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

STDCNCS

Desenvolvimento de estudo sobre a comunidade de cibersegurança em Portugal, no âmbito do Observatório de Cibersegurança

2021-2023

Sustainable HPC

Computação de elevado desempenho sustentável

2021-2025

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

Adding Records to Alloy

Authors
Brunel, J; Chemouil, D; Cunha, A; Macedo, N;

Publication
Rigorous State-Based Methods - 9th International Conference, ABZ 2023, Nancy, France, May 30 - June 2, 2023, Proceedings

Abstract
Records are a composite data type available in most programming and specification languages, but they are not natively supported by Alloy. As a consequence, users often find themselves having to simulate records in ad hoc ways, a strategy that is error prone and often encumbers the analysis procedures. This paper proposes a conservative extension to the Alloy language to support record signatures. Uniqueness and completeness is imposed on the atoms of such signatures, while still supporting Alloy’s flexible signature hierarchy. The Analyzer has been extended to internally expand such record signatures as partial knowledge for the solving procedure. Evaluation shows that the proposed approach is more efficient than commonly used idioms. © 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.

2023

Specifying Event/Data-based Systems

Authors
Knapp, A; Hennicker, R; Madeira, A;

Publication
RELATIONAL AND ALGEBRAIC METHODS IN COMPUTER SCIENCE, RAMICS 2023

Abstract
Event/data-based systems are controlled by events, their local data state may change in reaction to events. Numerous methods and notations for specifying such reactive systems have been designed, though with varying focus on the different development steps and their refinement relations. We first briefly review some of such methods, like temporal/modal logic, TLA, UML state machines, symbolic transition systems, CSP, synchronous languages, and Event-B with their support for parallel composition and refinement. We then present E. -logic for covering a broad range of abstraction levels of event/data-based systems from abstract requirements to constructive specifications in a uniform foundation. E. -logic uses diamond and box modalities over structured events adopted from dynamic logic, for recursive process specifications it offers (control) state variables and binders from hybrid logic. The semantic interpretation relies on event/data transition systems; specification refinement is defined by model class inclusion. Constructive operational specifications given by state transition graphs can be characterised by a single E. -sentence. Also a variety of implementation constructors is available in E. -logic to support, among others, event refinement and parallel composition. Thus the whole development process can rely on E. -logic and its semantics as a common basis.

2023

idDL2DL - Interval Syntax to dL

Authors
Santos, J; Figueiredo, D; Madeira, A;

Publication
Theoretical Aspects of Software Engineering - 17th International Symposium, TASE 2023, Bristol, UK, July 4-6, 2023, Proceedings

Abstract

2023

Recent Trends in Algebraic Development Techniques - 26th IFIP WG 1.3 International Workshop, WADT 2022, Aveiro, Portugal, June 28-30, 2022, Revised Selected Papers

Authors
Madeira, A; Martins, MA;

Publication
WADT

Abstract

2023

idDL2DL – Interval Syntax to $$d\mathcal {L}$$

Authors
Santos, J; Figueiredo, D; Madeira, A;

Publication
Theoretical Aspects of Software Engineering - Lecture Notes in Computer Science

Abstract

Facts & Figures

68Researchers

2016

21Senior Researchers

2016

1R&D Employees

2020

Contacts