Commit 44aeb25a authored by Teresa Carbajo-Garcia's avatar Teresa Carbajo-Garcia
Browse files

Update 2021-04-15-collegedefrance.md

parent 4135b7c0
Pipeline #203305 canceled with stages
......@@ -4,6 +4,6 @@ title: Talk at College de France, Philippa Gardner
Philippa Gardner gave a talk on Gillian: a Multi-language Platform for Compositional Symbolic Analysis at the [College de France](https://www.college-de-france.fr/site/institution/Le-College-Presentation.htm), as part of their Program logic seminars.
The talk was 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.
The talk was a general introduction to [Gillian](https://vtss.doc.ic.ac.uk/research/gillian.html), 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.
The video of the talk is available [on this link](https://www.college-de-france.fr/video/en-xavier-leroy/2021/sem-leroy-gardner-20210415.mp4).
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment