Program verification with F*

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

Lecture slides (9.12.2020)

Lab exercises (9-10.12.2020)

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

Homework

Useful code snippets

Sample solutions

Setup instructions

Using F* in your browser

Deploying F* on your computer

Using F* interactively

More references

Acknowledgements

The lecturer has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No 834146.