Tech talk at Galois, Philippa Gardner
Philippa Gardner was invited to give a tech talk at Galois, Portland, USA on Javert, a JavaScript Verification Toolchain.
JaVerT is a semi-automatic JavaScript Verification Toolchain based on separation logic aimed at the specialist developer wanting rich, mechanically verified specifications of critical JavaScript code. We address three main challenges: 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; finally the validation challenge is to understand what it means for the verification to be trusted.
You can see a video of the talk on the Galois Youtube channel.