Course at Summer School on Verification Technology, Systems, and Applications, VTSA 2019 at University of Luxembourg on 1-2 July 2019

**Teaching team**: Cătălin Hriţcu and Antoine Van Muylder

**Other contributors**: Danel Ahman and various other members of the F* team

Monday, 1 July 2019:

- 9:00--12:30
**A Gentle Introduction to F*: Verifying Purely Functional Programs**(slides) **Code:**- Fact.fst (factorial)
- Ackermann.fst (Ackermann function and decreases metrics)
- Rev.fst (list reversal)
- Divergence.fst (potentially divergent evaluator)
**Exercise 0:**Different types for incr (Incr.fst; solution: Incr.fst)**Exercise 1:**Summing 1 + 2 + 3 + ... (Sum.fst; solution: Sum.fst)**Exercise 2:**Refined stacks (RefinedStack.fst, RefinedStackClient.fst; solution: RefinedStack.fst, RefinedStackClient.fst)

Tuesday, 2 July 2019:

- 14:00--15:30
**Verifying Stateful Programs with F***(slides) **Code:**- IncrST.fst, Incr2ST.fst (increment function)
- SwapRefsST.fst (reference swapping)
- CountST.fst (stateful counting)
- FibonacciST.fst (stateful fibonacci)
- BufferAlloc.fst, BufferAlloc.c (low-level code)
**Exercise 1:**Sketch a hand proof of the correctness of integer reference swapping (SwapIntRefsST.fst)**Exercise 2:**Stateful summing 1 + 2 + 3 + ... (SumST.fst; solution)- 16:00--17:30
**Monotonic State in F***(slides) **Code:**- CounterMST.fst (monotonic counters)
- SimpleLogMST.fst (monotonic logs)
- InitFreezeMST.fst (initializable and freezable references)
- Snapshots.fst (escaping the preorder with snapshots)
**Exercise 1:**Typing of initializable and freezable references read and freeze actions (InitFreezeMST.fst; solution)

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.7.0-alpha1, most recent release) installed on their machine there are 2 easy options:

- Using the binary release (documentation on this)
- or Using the OPAM package
(especially for people already using OCaml; note that
in this case 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).