This page contains auxiliary material associated with the following paper at PLDI 2013:

This paper consolidates and extends work described in two MSR technical reports into a single conference submission.

  • Verification Condition Generation with the Dijkstra State Monad This report includes the metatheory of the Dijkstra state monad, including an elaboration into pure F*, a soundness theorem, a completeness theorem (of which the completeness result for JS* is a special case), and the first-order VC theorem.
  • Towards JavaScript Verification with the Dijkstra State Monad This report provides more details about each of our examples, including a description of the VC generation algorithm specialized for JS*. We also discuss (in Section 6) a query compilation procedure mentioned in our submission that shows how a certain class of higher-order VCs can be compiled to a sequence of first-order queries.

In addition to the technical reports above, we refer readers to the following code samples and downloads for more information about our work.

prims.fst: This F* module includes the signature of the Dijkstra State Monad, a main contribution of our submission. The specific variant we use here shows a Dijkstra monad carrying a rich two-state invariant on the heap, the use of the same monad to reason about exceptions, exception handlers, and fatal errors. This is a combination of the "iDST" and "eDST" monads described in the paper.

JSVerify.fst: This is an extended version of the JSPrims library shown in our submission. As mentioned in that paper, due to space limitations, we presented a simplified version of JavaScript semantics, ignoring prototype chains, getters/setters, functions-as-objects, and other features of the language. JSVerify.fst shows our full specification, incorporating all these features. We also show an implementation of the library, verified mechanically against its specification using F*'s typechecker for the Dijkstra state monad. As mentioned in the paper, JSVerify.fst is the foundation for a verified compiler from F* to JavaScript, proven fully abstract in a POPL 2013 paper, described here.

The latest download (version 0.6-alpha) of the F* compiler and verifier, together with all our examples is available here. In the download zip file, the examples relevant to our submission can be found in the following directories---a Makefile in the relevant directories indicates how the examples can be verified:

  • ex0--ex25 can be found in the directory examples/monadic
  • ac can be found in the file examples/monadic/authac.fst
  • automaton can be found in the file examples/monadic/automaton.fst
  • iflow can be found in the file examples/monadic/iflow.fst
  • auth can be found in the file examples/misc/auth.fst
  • auth2 can be found in the file examples/misc/auth2.fst
  • JSVerify can be found in the directory examples/jsverify
  • Untiny can be found in the file examples/monadic/js/Untiny.js
  • Delicious can be found in the file examples/monadic/js/Delicious.js
  • Passward can be found in the file examples/monadic/js/Passward.js
  • HoverMagn can be found in the file examples/monadic/js/HoverMagnifier.js
  • Typograf can be found in the file examples/monadic/js/Typograf.js
  • Facepalm can be found in the file examples/monadic/js/Facepalm.js

Forthcoming material:

  • An updated web-facing version of our compiler, with JS tools