---
title: JavaScript
project_id: web
menu: true
parent_menu: Research
menu_order: 4
sub_menu_order: 2
---

We study the mechanised specification of the JavaScript language
(following the ECMAScript 5 standard) and the verification of
JavaScript programs.

#### JSCert

With Bodin, Charguéraud, and Schmitt at Inria, we
have developed [JSCert](http://jscert.org/), a substantial Coq specification that is
line-by-line close to the core language of the ECMAScript 5
standard. It comes with a reference interpreter, JSRef, proven correct
with respect to JSCert and tested using the official Test262 test
suite. We are currently extending this specification to the
numerous libraries, providing continuous test integration for the
ever-growing specification, developing a new, human-readable JSRef,
with a tighter connection to the standard and good tracking
properties, and creating the web service Explain.js to explain
behavioural complexities of JavaScript programs.

#### JSIL

We have developed a principled compiler from JavaScript (ECMAScript 5
strict) to a small intermediate language JSIL, which has a simpler
operational semantics and is better suited to program verification.
The compiler has been substantially tested using the Test262 test
suite and it comes with a hand-proof of translation correctness 
for a fragment of the language. We will use JSIL to develop JSVerify - a
verification tool for JavaScript. Daiva Naudžiūnienė will
this year hold internships at Amazon and Facebook  to use
JSIL to develop front-ends for the CBMC and Infer verification tools.

#### Research Support

This research is supported by the EPSRC/GCHQ grant [EP/K032089/1]:
[Certified Verification of Client-Side Web Programs][1], the EPSRC
programme grant [EP/K008528/1]: [REMS: Rigorous Engineering of
Mainstream Systems][REMS] and previously by the EPSRC
programme grant [EP/H008373/2]: [Resource Reasoning].

We also interact extensively with [Arthur Charguéraud], [Alan Schmitt] and
[Martin Bodin] of INRIA, who are supported by the [AJACS] project.

[EP/K032089/1]: http://gow.epsrc.ac.uk/NGBOViewGrant.aspx?GrantRef=EP/K032089/1
[EP/H008373/2]: http://gow.epsrc.ac.uk/NGBOViewGrant.aspx?GrantRef=EP/H008373/2
[EP/K008528/1]: http://gow.epsrc.ac.uk/NGBOViewGrant.aspx?GrantRef=EP/K008528/1
[REMS]: http://www.cl.cam.ac.uk/~pes20/rems/
[1]: https://verificationinstitute.org/project/certified-verification-of-client-side-web-programs/
[Resource Reasoning]: http://www.resourcereasoning.com/
[Arthur Charguéraud]: http://www.chargueraud.org/
[Alan Schmitt]: https://www.irisa.fr/celtique/aschmitt/
[Martin Bodin]: http://people.irisa.fr/Martin.Bodin/index.html?lang=en
[AJACS]: http://ajacs.inria.fr/