< Retour au sommaire

Gillian – a compositional symbolic execution platform

Sacha-Élie Ayoun le

Lieu: bât 862, pièce 1073

Abstract

Gillian is a compositional symbolic execution platform, which allows for 3 kinds of analysis: 1) symbolic testing à la CBMC, 2) semi-automatic compositional verification of separation logic specifications à la Verifast, and 3) automatic compositional testing, based on bi-abduction, à la Infer Pulse. Gillian is parametric: it must be instantiated with a memory model written directly in OCaml. Parametrisation allows for great flexibility, and Gillian has been instantiated for JavaScript, C and Rust. In particular, Gillian allowed us to prove the same code written in both C and JavaScript, based on a common specification fragment, even though the two languages are very different. This presentation describes the workings of Gillian, the latest advances and the current work on the platform.

Résumé

Gillian est une plateforme d’execution symbolique compositionnelle qui permet 3 types d’analyse: 1) le test symbolique, à la CBMC, 2) la verification compositionnelle semi-automatique de specifications en logique de séparation, à la Verifast, et 3) le test automatique compositionnel, s’appuyant sur la bi-abduction, à la Infer et Pulse. La plateforme Gillian est paramétrique: elle doit être instanciée à l’aide d’un modèle mémoire écrit directement en OCaml. La parametrisation permet une grande flexibilité, et Gillian a été instanciée pour l’analyse de JavaScript, C et Rust. En particulier, Gillian a permit de prouver le même code écrit en C et en JavaScript, en se basant sur un fragment de specification commun, malgré les différences importantes entre les deux langages. Cette présentation décrit le fonctionnement de Gillian, les dernières avancées et le travail en cours sur l’évolution de la plateforme.