Towards an Axiomatic Verification System for JavaScript

Shengchao Qin; Aziem Chawdhary; Wei  Xiong; Malcolm  Munro; Zongyan Qiu; Huibiao Zhu

doi:10.1109/TASE.2011.33

Towards an Axiomatic Verification System for JavaScript

Shengchao Qin, Aziem Chawdhary, Wei Xiong, Malcolm Munro, Zongyan Qiu, Huibiao Zhu

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

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.

Original language	English
Title of host publication	2011 Fifth International Conference on Theoretical Aspects of Software Engineering
Publisher	IEEE
ISBN (Print)	978-1-4577-1487-0
DOIs	https://doi.org/10.1109/TASE.2011.33
Publication status	Published - 2011
Event	5th IEEE International Symposium on Theoretical Aspects of Software Engineering - Xi'an, China Duration: 29 Aug 2011 → 31 Aug 2011 Conference number: 5

Conference

Conference	5th IEEE International Symposium on Theoretical Aspects of Software Engineering
Abbreviated title	TASE 2011
Country/Territory	China
City	Xi'an
Period	29/08/11 → 31/08/11

Access to Document

10.1109/TASE.2011.33

Cite this

@inproceedings{d278412093484ab281907613de1f962e,

title = "Towards an Axiomatic Verification System for JavaScript",

abstract = "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.",

author = "Shengchao Qin and Aziem Chawdhary and Wei Xiong and Malcolm Munro and Zongyan Qiu and Huibiao Zhu",

year = "2011",

doi = "10.1109/TASE.2011.33",

language = "English",

isbn = "978-1-4577-1487-0",

booktitle = "2011 Fifth International Conference on Theoretical Aspects of Software Engineering",

publisher = "IEEE",

note = "5th IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2011 ; Conference date: 29-08-2011 Through 31-08-2011",

}

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

N1 - Conference code: 5

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 - http://dx.doi.org/10.1109/TASE.2011.33

U2 - 10.1109/TASE.2011.33

DO - 10.1109/TASE.2011.33

M3 - Conference contribution

SN - 978-1-4577-1487-0

BT - 2011 Fifth International Conference on Theoretical Aspects of Software Engineering

PB - IEEE

T2 - 5th IEEE International Symposium on Theoretical Aspects of Software Engineering

Y2 - 29 August 2011 through 31 August 2011

ER -

Towards an Axiomatic Verification System for JavaScript

Abstract

Conference

Access to Document

Other files and links

Fingerprint

Cite this