Gillian a Multi language Platform for Compositional (...)
summary
Gillian is a multi-language symbolic-analysis platform that currently supports JavaScript and C and uses a core symbolic execution engine plus a first-order solver backed by Z3. It compiles targets to a parametric intermediate language GIL with separate concrete and symbolic memory models. Results include found bugs in Buckets.js and Collections-C via symbolic testing and verified the AWS Encryption SDK deserialisation (170 LOC, one bug and one vulnerability fixed), with bounded proofs and bi-abduction for automatic compositional tests.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 6:55Gillian
- 9:05Memory Models
- 14:07Formalism
- 18:53General Correctness
- 19:43Memory Model
- 22:16Memory Model Formalism
- 25:39Evaluation
- 26:17correctness results
- 29:21future plans
- 32:35verification
related talks
16mCompositional Symbolic Execution for the Next 700 Memory Models
29mPartially Evaluating Symbolic Interpreters for All
48mCross-Domain Compilation: Exploiting Synergies Across the CS Community
21mCompositional pre-processing for automated reasoning in dependent type theory
22mA Vision of Miking: Interactive Programmatic Modeling, Language Composition, and Compilation
22mBoosting Compiler Testing by Injecting Real-World Code
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
21mGOOL: A Generic Object-Oriented Lanugage