Imperial College London
Portrait Picture

DrSergioMaffeis

Faculty of Engineering, Department of Computing

Senior Lecturer
 
 
 
//

Contact

 

+44 (0)20 7594 8390sergio.maffeis Website

 
 
//

Location

 

441Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@inproceedings{Gardner:2012:10.1145/2103656.2103663,
author = {Gardner, P and Maffeis, S and Smith, G and Gardner, PA and Maffeis, S and Smith, G},
doi = {10.1145/2103656.2103663},
pages = {31--44},
publisher = {ACM},
title = {Towards a program logic for JavaScript},
url = {http://dx.doi.org/10.1145/2103656.2103663},
year = {2012}
}
Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - JavaScript has become the most widely used language for clientsideweb programming. The dynamic nature of JavaScript makesunderstanding its code notoriously difficult, leading to buggy programsand a lack of adequate static-analysis tools. We believe thatlogical reasoning has much to offer JavaScript: a simple descriptionof program behaviour, a clear understanding of module boundaries,and the ability to verify security contracts.We introduce a program logic for reasoning about a broad subsetof JavaScript, including challenging features such as prototypeinheritance and with. We adapt ideas from separation logic toprovide tractable reasoning about JavaScript code: reasoning abouteasy programs is easy; reasoning about hard programs is possible.We prove a strong soundness result. All libraries written in oursubset and proved correct with respect to their specifications willbe well-behaved, even when called by arbitrary JavaScript code.
AU  - Gardner,P
AU  - Maffeis,S
AU  - Smith,G
AU  - Gardner,PA
AU  - Maffeis,S
AU  - Smith,G
DO  - 10.1145/2103656.2103663
EP  - 44
PB  - ACM
PY  - 2012///
SP  - 31
TI  - Towards a program logic for JavaScript
UR  - http://dx.doi.org/10.1145/2103656.2103663
UR  - http://doi.acm.org/10.1145/2103621.2103663
UR  - http://hdl.handle.net/10044/1/33265
ER  -
Download