Towards an Axiomatic Verification System for JavaScript
Shengchao Qin, Aziem Chawdhary, Wei Xiong, Malcolm Munro, Zongyan Qiu, Huibiao Zhu · 2011
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.