University of Cambridge > Talks.cam > Microsoft Research Cambridge, public talks > An introduction to program verification with F*

An introduction to program verification with F*

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact lecturescam.

Please note, this event may be recorded. Microsoft will own the copyright of any recording and reserves the right to distribute it as required.

Fstar (https://fstar-lang.org) is a verification-oriented programming language that follows in the tradition of ML. Like ML, Fstar is a typed, strict, and effectful functional programming language. However, Fstar type system is significantly richer than ML’s, allowing program specifications, including effects, to be stated and checked semi-automatically.

To prove that a program meets its type and effect specification, the Fstar type checker uses a weakest precondition calculus to compute verification conditions, which it then tries to discharge using the Z3 SMT solver. Crucially, there is no distinction between the language used to write programs and specifications. Consistency is maintained by verifying that specifications are pure, terminating computations.

This talk will be organized as a tutorial. I will gradually introduce the features of the language with the help of interactive demos. Some familiarity with functional programming languages, specially Fsharp or ML, can help, but it is not required.

Those willing to learn about advanced features of Fstar, like extraction to OCaml and C, verification of stateful programs using hyper heaps, and our ongoing work on verifying the TLS protocol, are welcome to stay after the first part of the talk.

This talk is part of the Microsoft Research Cambridge, public talks series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2017 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity