This work is joint with Jose Fragoso Santos, Petar Maksimovic and Sacha-Élie Ayoun.

I have been teaching an MSc course on Separation Logic for many years, with particular emphasis on the theory and tools for verifying algorithms for manipulating data structures represented in the heap. With my group, I have also spent several years developing a static analysis framework based on separation logic, which provides different strengths of reasoning from automatic bug-finding through to semi-automatic verification. Our work initially focussed on a specific framework, called JaVerT, for analysing of JavaScript programs, but has recently evolved into a general framework, called Gillian, for analysing programs from a range of languages. This lecture will provide a whirlwind tour of our five-year journey to develop Gillian, focussing on both the theory and tool development and using a selection of algorithms studied in my MSc course.

Philippa Gardner is a professor in the Department of Computing at Imperial College London and and has a UKRI Established Fellowship from 2018–2023. Her current research focusses on program verification: in particular, reasoning about Web programs (JavaScript and DOM); and reasoning about concurrent programs.

She completed her PhD thesis, supervised by Professor Gordon Plotkin FRS at Edinburgh in 1992 and held five years of fellowships at Edinburgh. She moved to Cambridge in 1998 on an EPSRC Advanced Fellowship, hosted by Professor Robin Milner FRS. She obtained a lectureship at Imperial in 2001, and became professor in 2009. She held a Microsoft Research Cambridge/Royal Academy of Engineering Senior Fellowship from 2005 to 2010 at Imperial.

Philippa Gardner is a professor in the Department of Computing at Imperial College London and and has a UKRI Established Fellowship from 2018–2023. Her current research focusses on program verification: in particular, reasoning about Web programs (JavaScript and DOM); and reasoning about concurrent programs.

She completed her PhD thesis, supervised by Professor Gordon Plotkin FRS at Edinburgh in 1992 and held five years of fellowships at Edinburgh. She moved to Cambridge in 1998 on an EPSRC Advanced Fellowship, hosted by Professor Robin Milner FRS. She obtained a lectureship at Imperial in 2001, and became professor in 2009. She held a Microsoft Research Cambridge/Royal Academy of Engineering Senior Fellowship from 2005 to 2010 at Imperial.

Philippa directs the Research Institute on Verified Trustworthy Software Systems (VeTSS), funded by EPSRC, from 2017 to 2022. She chaired the BCS awards committee, 2013-2018, which decides the Lovelace medal (senior) and Roger Needham award (mid-career) for computer science and engineering.