Show simple item record

dc.contributor.authorWatt, Conraden
dc.date.accessioned2018-03-21T15:04:23Z
dc.date.available2018-03-21T15:04:23Z
dc.date.issued2018-01-08en
dc.identifier.isbn9781450355865en
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/274174
dc.description.abstractWebAssembly is a new low-level language currently being implemented in all major web browsers. It is designed to become the universal compilation target for the web, obsoleting existing solutions in this area, such as asm.js and Native Client. The WebAssembly working group has incorporated formal techniques into the development of the language, but their efforts so far have focussed on pen and paper formal specification. We present a mechanised Isabelle specification for the WebAssembly language, together with a verified executable interpreter and type checker. Moreover, we present a fully mechanised proof of the soundness of the WebAssembly type system, and detail how our work on this proof has exposed several issues with the official WebAssembly specification, influencing its development. Finally, we give a brief account of our efforts in performing differential fuzzing of our interpreter against industry implementations.
dc.titleMechanising and verifying the WebAssembly specificationen
dc.typeConference Object
prism.publicationDate2018en
prism.publicationNameProceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofsen
dc.identifier.doi10.17863/CAM.21260
dcterms.dateAccepted2017-11-15en
rioxxterms.versionofrecord10.1145/3167082en
rioxxterms.versionAM*
rioxxterms.licenseref.urihttp://www.rioxx.net/licenses/all-rights-reserveden
rioxxterms.licenseref.startdate2018-01-08en
dc.contributor.orcidWatt, Conrad [0000-0002-0596-877X]
rioxxterms.typeConference Paper/Proceeding/Abstracten
pubs.funder-project-idEPSRC (EP/K008528/1)
pubs.funder-project-idEPSRC (1790117)
cam.issuedOnline2018-01-08en
pubs.conference-nameCPP '18: Certified Proofs and Programsen


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record