An introduction to program verification with F*

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

• Santiago Zanella-Beguelin, Microsoft Research Cambridge
• Thursday 14 July 2016, 10:30-11:15
• Small Lecture Theatre, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Guy Emerson's list
• Interested Talks
• Microsoft Research Cambridge, public talks
• Optics for the Cloud
• PMRFPS's
• School of Technology
• Small Lecture Theatre, Microsoft Research Ltd, 21 Station Road, Cambridge, CB1 2FB
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• personal list
• rp587

Note that ex-directory lists are not shown.