Program verification with F*

Guest lecture and accompanying lab sessions for the Advanced Programming Course (ITT8060) at the Tallinn University of Technology.

Lecture slides (12.12.2018)

Lab exercises (12-14.12.2018)

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

Verifying stateful programs

Verifying purely functional and stateful programs

Verifying monotonic stateful programs

Useful code snippets

Sample solutions

Setup instructions

Using F* in your browser

Deploying F* on your computer

Note: E.g., recent versions of F* use the [@expect_failure] attribute to denote the expectation of failing typechecking, while the v0.9.6.0 binary release uses the [@fail] attribute for the same purpose.

Using F* interactively

More references