Gillian: a Multi-language Platform for Compositional Symbolic Analysis

on YouTube ↗43m

" summary

Gillian is a multi-language symbolic-analysis platform that implements a core symbolic-execution engine backed by Z3, OCaml concrete and symbolic memory models, and a trusted compiler from target language to GIL. It supports whole-program symbolic testing, verification via separation logic (2K lines of annotations for a 170-line AWS deserialiser) and automatic compositional testing via bi-abduction. Instantiations for JavaScript and C find real bugs in Buckets.js, Collections-C and cash, produce a bounded correctness claim about event handlers (≤20 chars), and expose one bug plus one vulnerability in AWS code.

AI-written summary · about

" chapters (15)

1. 0:00Intro
2. 0:49VERIFIED SOFTWARE: JAVASCRIPT ANALYSIS
3. 1:08GILLIAN: UNIFIED SYMBOLIC ANALYSIS Technique
4. 9:12SYMBOLIC EXECUTION FORMAL SEMANTICS, CLOSELY FOLLOWED BY OCAM IMPLEMENTATION
5. 11:03ABSTRACTION USER INPUT: CORE PREDICATES Separation-logic assertions describing the memory building blocks Getter and setter functions for each core predicate
6. 15:51GENERAL CORRECTNESS RESULTS
7. 16:50GILLIAN-JS Trustworthy analysis of ECMAScript 5 Strict programs EXTENSIBLE OBJECT-PROPERTY MEMORY MODEL Structure heap, domain table, metadata table
8. 22:10GILLIAN-JS: SYMBOLIC EXECUTION USER INPUT: IS basic actions
9. 31:43FULL VERIFICATION: JAVASCRIPT AWS ENCRYPTION SDK TARGET CODE: AWS Encryption SDK message header manipulation CURRENT DEVELOPER APPROACH TO VALIDATION: concrete test suites, functions that assert program properties at runtime
10. 34:24AWS SDK MESSAGE HEADER A sequence of bytes, encoded as a JavaScript ArrayBuffer
11. 35:11SPECIFICATION: ENCRYPTION CONTEXT ENCRYPTION CONTEXT: serialised list of key value pairs
12. 36:47SPECIFICATION: EC KEY-VALUE MAP
13. 38:12SPECIFICATION: DECODEENCRYPTION CONTEXT
14. 39:41BUG: PROTOTYPE INHERITANCE
15. 41:29GILLIAN: A PLATFORM FOR UNIFIED SYMBOLIC ANALYSIS

" related talks

• 31mVerified Software at ScalePhilippa Gardner · O'Hearn Fest (POPL 2024)
• 01h 06mOn-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...Manuel Hermenegildo · LOPSTR 2023
• 47mExploring a complex codebase with AIJesús Espino · DevBcn 2025
• 24mSymbiotic: finding bugs in C programsMarek Chalupa · DevConf.CZ 2019
• 48mCross-Domain Compilation: Exploiting Synergies Across the CS CommunityTobias Grosser · VMIL 2021
• 01h 02mLanguage Design meets Verifying CompilersDavid J. Pearce · GPCE 2022
• 20mUnifying compositional verification and certified compilation with a three-dimensional(…)Yu Zhang, Zhong Shao, Yuting Wang, Jérémie Koenig · POPL 2025
• 15mA Low-Code Platform for Systematic Component-Oriented Language CompositionJérôme Pfeiffer, Andreas Wortmann · SLE 2023