Program verification with F*
Guest lecture and accompanying lab session for the Advanced Programming
Course (ITT8060) at the Tallinn University of
Technology.
Lecture slides (6.12.2023)
Lab exercises (67.12.2023)
These exercises are mostly independent of each other, so you do not need to do them in the given order, but the
earlier ones are generally more basic.
Out of all of them, Exercise 7 is probably the most involved. It lets you simultaneously practice the verification
of both pure and stateful programs.
Verifying purely functional programs
 Exercise 1: Summing 1 + 2 + 3 + ...
 Exercise 2: Simply typed stacks
 Exercise 3: Refined stacks
Verifying stateful programs
 Exercise 4: Stateful summing 1 + 2 + 3 + ...
 Exercise 5: Stateful factorial 1 * 2 * 3 * ...
 Exercise 6: Stateful Fibonacci 1 , 1 , 2 , 3 , 5 , 8 , ...
Verifying purely functional and stateful programs
 Exercise 7: Functional and mutable binary search trees
Verifying monotonic stateful programs
 Exercise 8: Initializable and freezable references
Homework
Useful code snippets
 Ackermann function, interfaces, and decreases metrics: Ackermann.fsti, Ackermann.fst
 List reversal: Rev.fst
 Potential divergence:Divergence.fst
 F*'s MLstyle garbagecollected memory model: FStar.Heap.fst, FStar.ST.fst
 F*'s lowlevel memory model: FStar.HyperStack.fst, FStar.HyperStack.ST.fst
 Stateful increment function: IncrST.fst, Incr2ST.fst
 Reference swapping: SwapRefsST.fst
 Stateful counting: CountST.fst
 Lowlevel code example: BufferAlloc.fst, BufferAlloc.c
 F*'s witnessed modality: FStar.Monotonic.Witnessed.fsti, FStar.Monotonic.Witnessed.fst
 F*'s monotonic MLstyle memory model: FStar.Monotonic.Heap.fst, FStar.ST.fst, FStar.Ref.fst
 F*'s monotonic lowlevel memory model: FStar.Monotonic.HyperStack.fst, FStar.HyperStack.ST.fst
 Classical logic in F*: FStar.Classical.fsti, FStar.Classical.fst, FStar.StrongExcludedMiddle.fst
 Monotonic counters: CounterMST.fst
 Monotonic logs: SimpleLogMST.fst
 Temporarily violating monotonicity with snapshots: Snapshots.fst
Sample solutions
Setup instructions
Using F* in your browser
Deploying F* on your computer

For people who want to get F* installed on their computer with little fuzz there are 2 easy options:
 Using the binary
releases
(documentation on
this):
 WARNING: The most recent (development) version of F* and its libraries are
often not compatible with these binary releases.
 Using the OPAM package
(especially for people already using OCaml):
 WARNING: As with the binary releases, the stable version of F* on OPAM is often
not compatible with with the most recent (develoment) version of F* and its libraries.
 In order to install the recent (development) version of F* through OPAM, please
follow the instructions.
 IMPORTANT: You need to additionally download and add to your PATH a supported
version of the Z3 SMTsolver, see the instructions.

People who are more motivated and more adventurous can of course also build F* directly from its sources, see the
documentation.
Using F* interactively

If you are familiar with the Emacs text editor,
it is recommended getting
fstarmode for it to make the most of F*'s interactive
features.

There is now also a new(ish) F* plugin for VS Code editor,
which supports both full and lax typechecking of F* code.
More references
Acknowledgements
The lecturer has received funding from the Air Force Office of Scientific Research under awards number
FA95502110024.