Philippa A. Gardner
Professor of Theoretical Computer Science
Philippa Gardner is a professor in the Department of Computing at Imperial College London and has a UK Research and Innovation Established Fellowship from 2018–2023. Her research focusses on program specification and verification. In particular, her group is credited with bringing logical abstraction and logical atomicity to modern concurrent separation logics, and is currently developing the Gillian platform for building symbolic analysis tools for real-world programming languages such as C and JavaScript, which unifies classical symbolic execution, semi-automatic verification based on separation logic, and automatic compositional testing based on bi-abduction.
Philippa directs the Research Institute on Verified Trustworthy Software Systems (VeTSS), funded by EPSRC and NCSC, 2017-2022. She is an organiser of the Isaac Newton Institute six-week summer programme on `Verified Software’, 2021.
Past Activities
Code Mesh V
13.45 - 14.25
Gillian: a Multi-language Platform for Compositional Symbolic Analysis
This work is joint with Petar Maksimovic, Jose Fragoso Santos and Sacha Ayoun.
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 a technique called bi-abduction. It uses a core symbolic execution engine with strong mathematical foundations that unifies bug catching and verification. So far, we have instantiated Gillian to JavaScript and C. These instantiations have already been successfully applied to real-world code: to find bugs in the data-structure libraries Buckets.js and Collections-C, to find bugs and prove bounded correctness results for a jQuery-like library, cash, and to verify the deserialisation function of the AWS Encryption SDK messaging system.
Publication:
Gillian, Part 1: A Multi-language Platform for Symbolic Execution, Jose Fragoso Santos, Peter Maksimovic, Sacha-Elie Ayoun, Philippa Gardner, PLDI’20. Part 2 is verification is currently being written.