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.

007

Projects

BringTrust

Strengthening CI/CD Pipeline Cybersecurity and Safeguarding the Intellectual Property

2025-2028

DisaggregatedHPC

Towards energy-efficient, software-managed resource disaggregation in HPC infrastructures

2025-2026

InfraGov

InfraGov: A Public Framework for Reliable and Secure IT Infrastructure

2025-2026

VeriFixer

VeriFixer: Automated Repair for Verification-Aware Programming Languages

2025-2026

ENSCOMP4

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

2024-2025

PFAI4_5eD

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

2024-2024

QuantELM

QuantELM: from Ultrafast optical processors to Quantum Extreme Learning Machines with integrated optics

2023-2024

Team
001

Laboratory

CLOUDinha

Publications

HASLab Publications

View all Publications

2022

Deploying Decentralized, Privacy-Preserving Proximity Tracing

Authors
Troncoso, C; Payer, M; Hubaux, JP; Salathé, M; Larus, JR; Bugnion, E; Lueks, W; Stadler, T; Pyrgelis, A; Antonioli, D; Barman, L; Chatel, S; Paterson, KG; Capkun, S; Basin, DA; Beutel, J; Jackson, D; Roeschlin, M; Leu, P; Preneel, B; Smart, NP; Abidin, A; Gürses, SF; Veale, M; Cremers, C; Backes, M; Tippenhauer, NO; Binns, R; Cattuto, C; Barrat, A; Fiore, D; Barbosa, M; Oliveira, R; Pereira, J;

Publication
COMMUNICATIONS OF THE ACM

Abstract
[No abstract available]

2022

Why3-do: The Way of Harmonious Distributed System Proofs

Authors
Lourenco, CB; Pinto, JS;

Publication
PROGRAMMING LANGUAGES AND SYSTEMS, ESOP 2022

Abstract
We study principles and models for reasoning inductively about properties of distributed systems, based on programmed atomic handlers equipped with contracts. We present the Why3-do library, leveraging a state of the art software verifier for reasoning about distributed systems based on our models. A number of examples involving invariants containing existential and nested quantifiers (including Dijsktra's self-stabilizing systems) illustrate how the library promotes contract-based modular development, abstraction barriers, and automated proofs.

2022

A tribute to Jose Manuel Valenca

Authors
Oliveira, JN; Pinto, JS; Barbosa, LS; Henriques, PR;

Publication
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING

Abstract
The present Special Issue of the Journal of Logical and Algebraic Methods in Programming was planned as a tribute to Jose Manuel Esgalhado Valenca on the occasion of his Jubilation. A tribute to a professor, in the deepest sense of the word, a colleague and a friend, but above all to a long and inspiring academic journey that has so profoundly shaped the development of Informatics as a scientific area in Portugal. A scientific area that, as he taught us, needs to be understood broadly: not only as an independent research domain, but also as an educational pillar, a strategy for social and economic development, a foundation for a multifaceted professional career. This preface introduces some steps of such a journey. The Special Issue features a selection of scientific papers written by his collaborators, colleagues and friends, covering the different areas Jose Valenca helped to launch and consolidate in Portugal, namely computational logic, verification and mechanized reasoning, and information security. (c) 2022 Published by Elsevier Inc.

2022

Picking Publication Targets

Authors
Baquero, C;

Publication
COMMUNICATIONS OF THE ACM

Abstract
The Communications website, http://cacm.acm.org, features more than a dozen bloggers in the BLOG@CACM community. In each issue of Communications , we'll publish selected posts or excerpts. twitter Follow us on Twitter at http://twitter.com/blogCACM http://cacm.acm.org/blogs/blog-cacm Carlos Baquero offers guidance on how to decide where to publish one's paper.

2022

Is Having AI Generate Text Cheating?

Authors
Baquero, C;

Publication
COMMUNICATIONS OF THE ACM

Abstract
Carlos Baquero on whether using artificial intelligence provides an unfair advantage to writers.

Facts & Figures

14Proceedings in indexed conferences

2020

16Academic Staff

2020

0Book Chapters

2020

Contacts