The Research Institute in Verified Trustworthy Software Systems (VeTSS) is the UK’s second Academic Research Institute in cyber security, funded by the Engineering and Physical Sciences Research Council (EPSRC) for five years, from April 2017.
The purpose of VeTSS is to bring together and support world-class UK academics, industrialists and government employees, unified by a common interest in software analysis, testing and verification. VeTSS stands at the forefront of research developments in fundamental theories and industrial-strength tools, targeting real-world applications. It succeeds the previous three-year Research Institute in Automated Program Analysis and Verification, funded by EPSRC and GCHQ. The National Cyber Security Centre (NCSC) anticipates giving approximately £2.5 million to VeTSS over five years to support academic research projects in software analysis, testing and verification.
This report provides a description of the projects funded by VeTSS. It demonstrates the deep connection between the VeTSS academic research, the standard bodies and industry. For example, Batty’s two VeTSS projects on understanding the concurrent behaviour of C++ have directly influenced the ISO C++ standard, and Livshits’s and Donaldson’s VeTSS project relates to an academic start-up of Donaldson that was bought by Google in 2018. This report also describes how VeTSS funding has led directly to a total of more than £10M of further funding from EPSRC, the EU, government bodies, and industry. For example, Yoshida’s work on her VeTSS project played a crucial part in her obtaining a £1.46M UKRI Established Career Fellowship, 2020-2025. Furthermore, the interaction between NCSC and VeTSS has led to an additional invited call by NCSC on “Verified High Assurance Software” in 2019.
We have held a number of events since the start of VeTSS, including our main annual workshop “Formal Methods and Tools for Security” at Microsoft Cambridge in September 2017 and 2018. This workshop was renamed into “Verified Software” and held at the Isaac Newton Institute in Cambridge in September, 2019 in preparation of the 2020 Newton Institute programme on “Verified Software” (delayed until 2022), organised by de Moura (Microsoft Redmond), Farzan (Toronto), Hoare (Microsoft), Gardner (Imperial), Larsen (Aalborg), Leroy (Inria Paris), McMillan (Microsoft Redmond), O’Hearn (Facebook and UCL), Sewell (Cambridge), Shankar (SRI, California, lead organiser) and Vardi (Rice). This meeting will bring international academics and industrialists to the UK for six weeks, laying the groundwork for the next generation of verification grand challenges. In anticipation of that meeting, two virtual workshops on “Verified Software: from Theory to Practice” will be held by the Newton Institute in the first half of 2021.
I hope that you will find this report of interest.
Professor Philippa Gardner Director of VeTSS