BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Understanding and Verifying Javascript Programs. -  Prof Philippa 
 Gardner - Imperial College London
DTSTART:20151202T140000Z
DTEND:20151202T150000Z
UID:TALK61547@talks.cam.ac.uk
CONTACT:David Greaves
DESCRIPTION:The behaviour of JavaScript programs executed in the browser i
 s\ncomplex.  This talk will describe two related projects: JSCert which\np
 rovides a mechanised specification of the JavaScript English standard\n(EC
 MAScript 5)\; and JSVerify which provides a verification tool for\nreasoni
 ng about Javascript programs. Both projects establish theory\nand tools fo
 r obtaining a better understanding of JavaScript programs.\nThe talk is ai
 med at a general audience interested in language\nspecification and progra
 m verification. Knowledge of JavaScript is not\nassummed.\n\nJSCert provid
 es a Coq mechanised specification of the core JavaScript\nlanguage. A key 
 aim is to develop a methodology for establishing\ntrust. The JSCert specif
 ication is line-by-line close to the\nJavaScript English standard. It come
 s with a reference interpreter\,\nJSRef\, which is proven correct with res
 pect to JSCert and tested using\nthe official Test262 test suite.  In this
  talk\, I will describe and\nevaluate the current state of the JSCert proj
 ect.\n\nJSVerify provides a verification tool for reasoning about JavaScri
 pt\nprograms (in ECMAScript 5 strict mode)\, based on a principled compile
 r\nfrom JavaScript to an intermediate language called JSIL. JSIL has\nesse
 ntially the same memory model as JavaScript but a simpler\nspecification w
 hich reduces the workload required to build and adapt\nanalysis tools. The
  compiler has been substantially tested using the\nTest262 test suite and 
 a fragment has been proved correct. In this\ntalk\, I will describe JSVeri
 fy and current plans to build JavaScript\nfront-ends for the analysis tool
 s CBMC (Amazon)\, Infer (Facebook) and\nViper (ETH).\n\nAn ultimate challe
 nge is to verify the verifier\, checking that the\nproofs developed by JSV
 erify are indeed correct using JSCert.\n
LOCATION:Lecture Theatre 1\, Computer Laboratory
END:VEVENT
END:VCALENDAR