'Gillian Verification of JavaScript and C', Tech Talk by Philippa Gardner and Petar Maksimović

"Gillian Verification of JavaScript and C", Galois Tech Talk by Philippa Gardner and Petar Maksimović, 2021-05-05

Philippa Gardner is a Professor in the Department of Computing at Imperial College London and a Fellow of the Royal Academy of Engineering. She currently holds a UK Research and Innovation Established Fellowship and directs the Research Institute on Verified Trustworthy Software Systems (VeTSS), funded by EPSRC and NCSC. Her research focusses on program testing and verification. In particular, her group is credited with bringing logical abstraction and logical atomicity to modern concurrent separation logics, developing trusted Coq-mechanised specifications of programming languages such as JavaScript and Web Assembly, and developing the Gillian platform for building symbolic-analysis tools for real-world programming languages such as JavaScript and C.

Petar Maksimović is a Research Fellow in the Department of Computing at Imperial College London. His expertise lies in the design and implementation of program analysis tools, including the JaVerT framework for the analysis of JavaScript programs, and the Gillian platform which unifies testing and verification.

Gillian, Part I: A Multi-language Platform for Symbolic Execution, José Fragoso Santos, Petar Maksimović, Sacha-Élie Ayoun, Philippa Gardner, PLDI’20.

Gillian, Part II: Real-World Verification for JavaScript and C, Petar Maksimović, Sacha-Élie Ayoun, José Fragoso Santos, Philippa Gardner, CAV’21.