A Trusted Mechanised Specification of JavaScript: One Year On
Venue
Proceedings of the 27th International Conference on Computer Aided Verification (CAV’15), pp. 3–10
Publication Year
2015
Identifiers
Authors
- Philippa Gardner
- Gareth Smith
- Conrad Watt
- Thomas Wood
Abstract
The JSCert project provides a Coq mechanised specification of the core JavaScript language. A key part of the project was to develop a methodology for establishing trust, by designing JSCert in such a way as to provide a strong connection with the JavaScript standard, and by developing JSRef, a reference interpreter which was proved correct with respect to JSCert and tested using the standard Test262 test suite. In this paper, we assess the previous state of the project at POPL’14 and the current state of the project at CAV’15. We evaluate the work of POPL’14, providing an analysis of the methodology as a whole and a more detailed analysis of the tests. We also describe recent work on extending JSRef to include Google’s V8 Array library, enabling us to cover more of the language and to pass more tests.