Program verification with F*

Course at 2018 EUTypes Summer School on Types for Programming and Verification in Ohrid, Macedonia on 8-12 August, 2018

(Based on past courses by Cătălin Hriţcu and various other members of the F* team)


Friday, 10 August, 2018:

Saturday, 11 August, 2018:

Sunday, 12 August, 2018:

Setup instructions

The easiest way to try out F* quickly is directly in your browser using the online editor that's part of the F* tutorial.

We also have an even cooler online editor (experimental).

For people who want to get F* (v0.9.6.0, most recent release) installed on their machine there are 2 easy options:

  1. Using the binary release (documentation on this)
  2. or Using the OPAM package (especially for people already using OCaml; note that you still need to get Z3 separately)

In addition, if you're familiar with emacs, we recommend getting fstar-mode for it.

For people who are more motivated, there are even more ways including building F* from sources (see documentation on this).

Note: Recent versions of F* use the [@expect_failure] attribute to denote the expectation of failing typechecking, while the v0.9.6.0 release uses the [@fail] attribute for the same purpose. Change this according to the version you use, e.g., this concerns Ackermann.fst.

More references