This talk will give a general introduction to Gillian, a multi-language platform for symbolic program analysis being developed by my team at Imperial College London. Gillian currently supports three types of analysis: whole-program symbolic testing; full verification based on separation logic; and automatic compositional testing based on bi-abduction. It uses a core symbolic execution engine, with strong mathematical foundations, that unifies bug catching and verification. To instantiate Gillian to a new target language (TL), the tool developer must provide: a compiler from the TL to GIL, an intermediate representation which is parametric on the TL memory model: that is, on the set of basic actions capturing the ways in which TL programs fundamentally interact with their memories; an OCaml implementation of the TL memory model using the basic actions; proofs of simple lemmas for the TL basic actions, if interested in correctness guarantees. So far, we have instantiated Gillian to JavaScript and C. These instantiations have been used to: find bugs in the real-world data-structure libraries Buckets.js and Collections-C; find bugs and prove bounded correctness results for a real-world jQuery-like library, cash; and verify the deserialisation function of the AWS Encryption SDK messaging system.

The discussion and AMA following this talk will be moderated by Jan Vitek.

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.