A Trusted Mechanised Specification of JavaScript: One Year On
Author(s)
Gardner, P
Smith, G
Watt, C
Wood, T
Type
Conference Paper
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.
Date Issued
2015-07-16
Date Acceptance
2015-05-26
Citation
Computer Aided Verification: 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, 2015, 9206, pp.3-10
ISBN
978-3-319-21690-4
ISSN
0302-9743
Publisher
Springer
Start Page
3
End Page
10
Journal / Book Title
Computer Aided Verification: 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I
Volume
9206
Copyright Statement
© 2015, Springer International Publishing Switzerland. The final publication is available at Springer via https://dx.doi.org/10.1007/978-3-319-21690-4_1
Source
27th International Conference on Computer Aided Verification
Publication Status
Published
Start Date
2015-07-18
Finish Date
2015-07-24
Coverage Spatial
San Francisco, California