AutoPaSS: Automatic verification of complex privacy requirements in unbounded-size secure systems

Today’s devices execute tasks concurrently in numerous and hyper-connected ways, so we need reliable system-analysis techniques which capture not only cybersecurity properties but also modern connectivity.

Start date

July 2019

End date

June 2022


The need for reliable system-analysis techniques becomes an even bigger challenge if we need to robustly analyse rich and complex properties such as anonymity and users’ untraceability.

The aim of the AutoPaSS project is to address this gap in the formal verification of secure systems. In the project, a team led by Dr Ioana Boureanu will develop formal methods and software-tools needed to analyse security and, especially, privacy in modern communications systems.

Funding amount





  • Vector GB Ltd
  • Thales.