We are pleased to announce JSCert, a formalisation of Chapters 8-14 of
the ES5 standard. 

We've built JSCert using the Coq proof assistant, using the same
metaphors and data structures as the ES5 standard, and following ES5
algorithm listings line-by-line. This means we can evolve our formalism
along with ECMAScript: local changes to the standard should mean
similarly local changes to JSCert. At the same time, we've structured
JSCert to make it as easy as possible to build analysis and verification
tools on top.

We also provide JSRef, an interpreter for ES5, which we have verified in
Coq to correctly implement JSCert. We have also tested JSRef using
test262. Since each line of JSRef has a close correspondence with a
given line of JSCert and the ES5 algorithms we will be able to use code
coverage tools to begin to evaluate how much of ES5 is covered by
test262.

We very much hope that people will be interested in using JSCert and
JSRef for investigating, for example, semantics-preserving compilation
to ECMAScript, or other language analyses.

You can find papers, code, talks and docs all at our website:

http://jscert.org

The code is here:

http://github.com/jscert/jscert

And our recent paper describing the project is here:

http://www.doc.ic.ac.uk/~gds/jscert_popl14.pdf

Thanks,

Gareth

We are pleased to announce JSCert, a formalisation of Chapters 8-14 of
the ES5 standard. 

We've built JSCert using the Coq proof assistant, using the same
metaphors and data structures as the ES5 standard, and following ES5
algorithm listings line-by-line. This means we can evolve our formalism
along with ECMAScript: local changes to the standard should mean
similarly local changes to JSCert. At the same time, we've structured
JSCert to make it as easy as possible to build analysis and verification
tools on top.

We also provide JSRef, an interpreter for ES5, which we have verified in
Coq to correctly implement JSCert. We have also tested JSRef using
test262. Since each line of JSRef has a close correspondence with a
given line of JSCert and the ES5 algorithms we will be able to use code
coverage tools to begin to evaluate how much of ES5 is covered by
test262.

We very much hope that people will be interested in using JSCert and
JSRef for investigating, for example, semantics-preserving compilation
to ECMAScript, or other language analyses.

You can find papers, code, talks and docs all at our website:

http://jscert.org

The code is here:

http://github.com/jscert/jscert

And our recent paper describing the project is here:

http://www.doc.ic.ac.uk/~gds/jscert_popl14.pdf