Gareth Smith (Imperial College London): Local Reasoning for JavaScript

Abstract: We define separation logic rules that enable local reasoning for a small but representative subset of the standardized core of JavaScript. Our rules are sound in all JavaScript computational contexts, which means that we can reason about soundness properties of library code which may be called by arbitrary real-world JavaScript programs. With examples we illustrate the trade-off between complexity and expressiveness of local reasoning for this language.