Abstract:
We will give a general introduction to Gillian, a platform for the development of symbolic-execution tools for many programming languages. 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. 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; to find bugs and prove bounded correctness results for a real-world jQuery-like library, cash; and to verify the deserialisation function of the AWS Encryption SDK messaging system, implemented in Javascript and C. We will focus on Gillian verification for this talk.
Bio:
Philippa Gardner, joint with Petar Maksimović, José Fragoso Santos and Sacha-Élie Ayoun. The talk will be given by Gardner and Maksimović.
Philippa Gardner is a Professor in the Department of Computing at Imperial College London and a Fellow of the Royal Academy of Engineering. She currently holds a UK Research and Innovation Established Fellowship and directs the Research Institute on Verified Trustworthy Software Systems (VeTSS), funded by EPSRC and NCSC. Her
research focusses on program testing and verification. In particular, her group is credited with bringing logical abstraction and logical atomicity to modern concurrent separation logics, developing trusted Coq-mechanised specifications of programming languages such as JavaScript and Web Assembly, and developing the Gillian platform for building symbolic-analysis tools for real-world programming languages such as JavaScript and C.
Petar Maksimović is a Research Fellow in the Department of Computing at Imperial College London. His expertise lies in the design and implementation of program analysis tools, including the JaVerT framework for the analysis of JavaScript programs, and the Gillian platform which unifies testing and verification.
Publications:
Gillian, Part I: A Multi-language Platform for Symbolic Execution, José Fragoso Santos, Petar Maksimović, Sacha-Élie Ayoun, Philippa Gardner, PLDI’20.
Gillian, Part II: Real-World Verification for JavaScript and C, Petar Maksimović, Sacha-Élie Ayoun, José Fragoso Santos, Philippa Gardner, CAV’21.
Galois was pleased to host this tech talk via live-stream for the public. A video of the presentation can be found above.