Biography
I am Sacha, PhD Student at Imperial College under the supervision of Philippa Gardner and a member of the Verified Trustworthy Software Specification Group . I am working on Gillian, a parametric symbolic execution tool for symbolic testing, verification and automatic compositional testing. My full CV is available..
In my free time, I try to contribute to some open-source projects I love. I am an OCaml enthusiast, amateur magician and I like to rollerblade my way through London.
Publications
Committees and Panels
Teaching
- Tutorial Helper
- Coursework writing
- Coursework marking
- Exam question design
- Tutorial Helper
- Coursework marking
- Tutorial Helper
- Coursework marking
- Tutorial Helper
- Coursework marking
- Group project supervision
- Project marking
- Tutorial Helper
- Group tutoring
Supervision
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 project was awarded the Distinguished status.
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.