Résumé
Le dernier séminaire de l'année, présenté en anglais, a décrit la plate-forme multilangages Gillian de vérification par exécution symbolique et ses utilisations pour vérifier et pour trouver des erreurs dans des bibliothèques JavaScript et C.
Philippa Gardner gave a general introduction to Gillian, a multi-language platform for the development of symbolic-execution tools. 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, the Gillian team has instantiated Gillian to JavaScript and C, languages with substantially different memory models. 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.
This work is joint with Petar Maksimovic, Jose Fragoso Santos and Sacha Ayoun.
