TY - GEN
T1 - Towards an axiomatic verification system for JavaScript
AU - Qin, Shengchao
AU - Chawdhary, Aziem
AU - Xiong, Wei
AU - Munro, Malcolm
AU - Qiu, Zongyan
AU - Zhu, Huibiao
PY - 2011
Y1 - 2011
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/80055101638
U2 - 10.1109/TASE.2011.33
DO - 10.1109/TASE.2011.33
M3 - 会议稿件
AN - SCOPUS:80055101638
SN - 9780769545066
T3 - Proceedings - 5th International Conference on Theoretical Aspects of Software Engineering, TASE 2011
SP - 133
EP - 141
BT - Proceedings - 5th International Conference on Theoretical Aspects of Software Engineering, TASE 2011
T2 - 5th International Conference on Theoretical Aspects of Software Engineering, TASE 2011
Y2 - 29 August 2011 through 31 August 2011
ER -