Towards an Axiomatic Verification System for JavaScript

JavaScript as a Web scripting language has been widely used following the fast growth of Internet. Due to the flexible and dynamic features offered by the JavaScript language, it has become a challenging problem to statically reason about code written in JavaScript. As a first step towards building a mechanised verification system for JavaScript, we present, in this paper, an axiomatic verification system for a core subset of JavaScript based on a variant of separation logic. We have also defined a big-step operational semantics with respect to which we have demonstrated the soundness of our verification system.