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.