Understanding and Verifying Javascript Programs.

Add to your list(s) Download to your calendar using vCal

• Prof Philippa Gardner - Imperial College London
• Wednesday 02 December 2015, 14:00-15:00
• Lecture Theatre 1, Computer Laboratory.

If you have a question about this talk, please contact David Greaves.

The behaviour of JavaScript programs executed in the browser is complex. This talk will describe two related projects: JSCert which provides a mechanised specification of the JavaScript English standard (ECMAScript 5); and JSVerify which provides a verification tool for reasoning about Javascript programs. Both projects establish theory and tools for obtaining a better understanding of JavaScript programs. The talk is aimed at a general audience interested in language specification and program verification. Knowledge of JavaScript is not assummed.

JSCert provides a Coq mechanised specification of the core JavaScript language. A key aim is to develop a methodology for establishing trust. The JSCert specification is line-by-line close to the JavaScript English standard. It comes with a reference interpreter, JSRef, which is proven correct with respect to JSCert and tested using the official Test262 test suite. In this talk, I will describe and evaluate the current state of the JSCert project.

JSVerify provides a verification tool for reasoning about JavaScript programs (in ECMA Script 5 strict mode), based on a principled compiler from JavaScript to an intermediate language called JSIL . JSIL has essentially the same memory model as JavaScript but a simpler specification which reduces the workload required to build and adapt analysis tools. The compiler has been substantially tested using the Test262 test suite and a fragment has been proved correct. In this talk, I will describe JSVerify and current plans to build JavaScript front-ends for the analysis tools CBMC (Amazon), Infer (Facebook) and Viper (ETH).

An ultimate challenge is to verify the verifier, checking that the proofs developed by JSVerify are indeed correct using JSCert.

This talk is part of the Wednesday Seminars - Department of Computer Science and Technology series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Chris Davis' list
• Department of Computer Science and Technology talks and seminars
• Graduate-Seminars
• Guy Emerson's list
• Interested Talks
• Lecture Theatre 1, Computer Laboratory
• School of Technology
• Trust & Technology Initiative - interesting events
• Wednesday Seminars - Department of Computer Science and Technology
• bld31
• computer science
• se393's list

Note that ex-directory lists are not shown.