Sacha-Élie Ayoun, Postdoctoral researcher at Imperial College London.

This project extends Gillian with continuous reasoning foundations that substantially advance its applicability to real-world projects. In particular, Alexis has: extended its instantiations for C and JavaScript in order to allow them to analyse multi-file projects; and incorporated a mechanism for re-using previously-stored results in order to focus analysis on only the fragments of the source program that have changed. Finally, by analysing two real-world C and JavaScript projects, Alexis has demonstrated the significant improvement in the usability of Gillian by a general developer, as well as the correctness of our implementation.

This projects lays out the foundations for a reporting system for Gillian that systematically organises the reports produced by Gillian into a hierarchical structure over which the Gillian developer has full control; reporters that can export that hierarchical structure into useful formats, such as textual log files and database reports and a language-specific reporting mechanism that the Gillian developer can easily instantiate for their target language of choice

This project presents an interactive debugger for Gillian, building on the infrastructured built by Radu Lacraru in his project. It is incorporated into the Visual Studio Code editor and substantially improves the experience of developing and using the tool. Therefore, this project constitutes the first, essential step towards bringing the platform closer to students and general programmers. As part of the project, Matthew improved and structured the existing general mechanism for creating and storing queryable log traces during Gillian's symbolic execution, and used this mechanism to power the debugger as well as to provide an interface for parametric lifting of error messages from Gillian's intermediate representation to the level of the target language.

This project received a Distinction grade.

Based on Matthew Ho’s and Radu Lacraru’s work, Nat pushed Gillian’s debugging experience to an entirely new league. He used the queryable log traces to their full potential, and designed a new interface, integrated in VSCode, to debug symbolic execution assertion unification. This interface is a strong step towards the improvement of the interactivity of Gillian.

This project was awarded the Distinguished status, and Nat joined our group as a research engineer to help improving Gillian.

In this project, Opale extended the formalism from my PhD thesis to use resource algebras (from Iris) instead of partial commutative monoid. The formalism propose a way of composing together state models for Gillian as to simplify the creation of correct-by-construction compositional symbolic execution engines for different languages.

In addition, she also implemented all of the proposed transformers within Gillian (which was not done in my thesis) and replaced the existing state models with transformer-based ones. In turn, she found interesting optimisations which applied to all these state models and managed to get speedups for all supported languages.