Program verification with F*

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

Schedule

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)

Code and exercises from slides

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.7.0-alpha1, 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 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).

More references

• F* website
• F* tutorial
• F* code on GitHub
• KreMLin compiler for Low*
• Project Everest