Towards a program logic for JavaScript

By Philippa Gardner, Sergio Maffeis, Gareth Smith. 2012

91 citations recorded by the source corpus.

JavaScript has become the most widely used language for client-side web programming. The dynamic nature of JavaScript makes understanding its code notoriously difficult, leading to buggy programs and a lack of adequate static-analysis tools. We believe that logical reasoning has much to offer JavaScript: a simple description of program behaviour, a clear understanding of module boundaries, and the ability to verify security contracts. We introduce a program logic for reasoning about a broad subset of JavaScript, including challenging features such as prototype inheritance and "with". We adapt ideas from separation logic to provide tractable reasoning about JavaScript code: reasoning about easy programs is easy; reasoning about hard programs is possible. We prove a strong soundness result. All libraries written in our subset and proved correct with respect to their specifications will be well-behaved, even when called by arbitrary JavaScript code.

Subfields: Artificial Intelligence, Signal Processing

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

  1. Panagiotis Vekris
  2. Benjamin Cosman
  3. Ranjit Jhala
  4. Gavin M. Bierman
  5. Martín Abadi
  6. Mads Torgersen
  7. David Herman
  8. Ravi Chugh

In Signal Processing

  1. Ranjit Jhala
  2. Martín Abadi

Citations in the corpus