Abstract:
The dynamic nature of JavaScript and its complex semantics make it a difficult target for logic-based verification. In this talk, I will describe JaVerT, a semi-automatic JavaScript Verification Toolchain
based on separation logic. JaVerT is aimed at the specialist developer wanting rich, mechanically verified specifications of critical JavaScript code. The specification challenge is to design specifications that are readable by developers. The verification challenge is to handle the complex, dynamic nature of JavaScript without simplification. The validation challenge is to understand what it means for the verification to be trusted.
Bio:
Philippa Gardner is a professor in the Department of Computing at Imperial College London and leader of the research group working on Verified Trustworthy Software Specification. Her current research focusses on reasoning about web programs (JavaScript and DOM); and reasoning about concurrent programs.
She completed her PhD thesis, supervised by Professor Gordon Plotkin FRS at Edinburgh in 1992. She moved to Cambridge in 1998 on an EPSRC Advanced Fellowship, hosted by Professor Robin Milner FRS. She obtained a lectureship at Imperial in 2001, and became professor in 2009. She held a Microsoft Research Cambridge/Royal Academy of Engineering Senior Fellowship from 2005 to 2010 at Imperial.
Philippa directs the Research Institute on Verified Trustworthy Software Systems (VeTSS), funded by EPSRC, from 2017 to 2022. She also chairs the BCS awards committee, which decides the Lovelace medal (senior) and Roger Needham award (mid-career) for computer science and engineering.