High-Assurance Software

About Domain

At the High-Assurance Software Laboratory (HASLab), we improve practice through theory, creating and implementing software that goes beyond mere functionality: we ensure it is correct, resilient, and secure against failures and attacks. Our team of researchers, scientists, and engineers has proven expertise in software engineering, developing methods and tools to design and integrate robust software; in distributed systems, exploring distribution and replication to ensure scalability and reliability; and in information security, addressing cybersecurity challenges and improving systems with advanced, secure cryptographic protocols, thus minimising vulnerabilities. With a multidisciplinary approach supported by solid theoretical principles, we develop innovative solutions for critical software, secure cloud infrastructures, and privacy-aware big data management, driving scientific advancement, innovation, and high-level consultancy. In addition, we complement our core expertise with work in human-computer interaction, programming languages, computational mathematics, and quantum computing - because we believe the future of trustworthy software is built on knowledge and innovation.

Flagship Projects

PeT

EPICURE

See more projects

Selected Publications

Formally Verifying Kyber - Episode V: Machine-Checked IND-CCA Security and Correctness of ML-KEM in EasyCrypt

Almeida, JB;Olmos, SA;Barbosa, M;Barthe, G;Dupressoir, F;Grégoire, B;Laporte, V;Léchenet, JC;Low, C;Oliveira, T;Pacheco, H;Quaresma, M;Schwabe, P;Strub, PY;

2024

Advances in Cryptology - CRYPTO 2024 - 44th Annual International Cryptology Conference, Santa Barbara, CA, USA, August 18-22, 2024, Proceedings, Part II

Databases in Edge and Fog Environments : A Survey

Meruje Ferreira, LM;Coelho, F;Pereira, J;

2024

ACM Computing Surveys

Point-free program transformation

Cunha, A;Pinto, JS;

2005

FUNDAMENTA INFORMATICAE

Recursion patterns and time-analysis

Barbosa, A;Cunha, A;Pinto, JS;

2005

ACM SIGPLAN NOTICES

See more publications

Team Members

Team Leaders

Alcino Cunha

Alcino Cunha is Associate Professor at the Department of Informatics of University of Minho and a member (and currently co-coordinator) of the High-Assurance Software Laboratory, a research center of the INESC TEC associate laboratory. His research focuses on making formal software design more accessible for all software engineers, and he was one of the main developers of the new version 6 of the Alloy lightweight formal method, that added support for behavioral specifications and temporal logic. He is also interested in the topic of robotic software quality, namely developing formal analysis tools for software developed with the popular ROS framework. He published over 70 papers, including several papers in relevant software engineering and robotic venues, such as TSE, FSE, ASE, IROS, or FM.

António Luís Sousa

I am an Assistant Professor at the Department of Informatics of the University of Minho and a Senior Researcher at HASLab/INESC TEC.

My research interests are in dependable distributed systems, in particular with application to dependable distributed database systems, large scale distributed systems and cloud computing management.