
High-Assurance Software
About the Centre
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.
Centre Areas

Segurança da Informação
Our research in Information Security combines rigorous theoretical foundations with innovative practical approaches. We aim to build secure systems with formal guarantees, bridging the development of cryptographic protocols with their efficient and reliable implementation. On the theoretical side, we work with security proofs and computer-assisted cryptography, developing formal techniques that automatically validate security properties. On the applied side, we focus on implementations that meet high standards of performance and security, ensuring that theoretical guarantees are preserved from specification through to final code. To achieve this, we design domain-specific languages and tools that facilitate the development of highly trustworthy cryptographic software. We also investigate advanced threat detection and response mechanisms, which are essential to continuously preserving the security properties of systems. Our solutions are applicable to several domains, including privacy-preserving technologies, secure data storage, and cloud computing — all critical areas for ensuring security in the digital age.

Sistemas Distribuídos
In Distributed Systems, we are transforming the way data is managed in cloud computing, critical systems, advanced computing infrastructures, and artificial intelligence ecosystems. We explore new frontiers in reliability, replication, and data distribution, developing novel consensus protocols and conflict-free approaches to eventual consistency, ensuring data integrity through replicated data types. We optimise the processing of transactional and analytical workloads in databases and create secure methods for handling data in untrusted environments, enhancing the resilience and security of systems. Learn more here. We design efficient data storage solutions capable of keeping up with the rapid growth of digital information. We use modern technologies to meet the demands for performance, scalability, reliability, security, and energy efficiency. Discover more here. We develop middleware systems with a focus on semantic interoperability, applied to real-world use cases and data spaces. Our mission is to shape the future of distributed data management, with solutions for the next generation of digital services.

Engenharia de Software
The Software Engineering area aims to develop novel methods, techniques, and tools that advance how software is designed, constructed, and assessed. It seeks to ensure that the research results have a lasting impact on software development practices and contribute to improving the industry’s competitiveness. The main research lines are: 1) software requirements, design, and construction: requirements management, software architecture and design, model-driven development, and cloud-native software engineering; 2) software testing: model-based testing, mobile testing, distributed systems testing, and IoT testing; 3) software process and tools: agile processes, process improvement, tools for collaboration and knowledge management; serious games in software engineering education. Within these research lines, we aim to continue to identify, get to the essence, and document what actually constitutes good solutions in modern-day software engineering, working closely with professionals; and continuing to advance the state of the art in techniques, practices, and tools that can, in different ways, improve the effectiveness, efficiency, and experience of software developers.
Flagship Projects
Team Members
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
Loading Loading Loading Loading
Loading Loading Loading Loading
Loading Loading Loading Loading
Loading Loading Loading Loading
Loading Loading Loading Loading
Loading Loading Loading Loading
Loading Loading Loading Loading
Loading Loading Loading Loading
Loading Loading Loading Loading
Loading Loading Loading Loading
News & Events
Loading Loading Loading Loading Loading Loading Loading Loading Loading
Loading Loading Loading Loading Loading Loading Loading Loading Loading
Loading Loading Loading Loading Loading Loading Loading Loading Loading
Loading Loading Loading Loading Loading Loading Loading Loading Loading
Loading Loading Loading Loading Loading Loading Loading Loading Loading
Loading Loading Loading Loading Loading Loading Loading Loading Loading
Loading Loading Loading Loading Loading Loading Loading Loading Loading
Loading Loading Loading Loading Loading Loading Loading Loading Loading
Loading Loading Loading Loading Loading Loading Loading Loading Loading
Supervised Theses
Cybersecurity analysis of a SCADA system under current standards, penetration testing and definition of mitigating strategies
Filipe Pestana Duarte Rocha
M - 2019
UP-FEUP
Monitorização de um Sistema Publish-Subscribe ROS para Enumeração e Deteção de Intrusões
João Pedro Xavier Araújo
M - 2019
UP-FEUP
Deteção de nomes de domínios gerados aleatoriamente
António Jorge Aguiar do Vale
M - 2019
UP-FEUP
Computação Paralela na Análise de Tráfego de Redes de Comunicação
Tiago Samuel da Rocha Silva
M - 2019
UP-FEUP
Contact Us
Get in touch with us. We will respond as soon as possible.










