Tue 19 Jun 2018 14:00 - 15:40 at Discovery C - Verified Low-Level Programming in F*
Tue 19 Jun 2018 16:10 - 17:35 at Discovery C - Verified Low-Level Programming in F*

F* is an ML-like programming language aimed at program verification. At its core is a type system based on dependent types, refinement types and Hoare-style logics for user-defined monadic effects. Together, these features allow expressing precise and compact specifications for programs, including functional correctness and security properties. The F* type-checker aims to prove that programs meet their specifications using a combination of SMT solving, user provided proof terms, as well as interactive proofs using tactics.

This tutorial provides a general introduction to F* followed by a focus on Low*, a subset of F* that extracts to C code for efficient, low-level programming. The examples we present are drawn from Project Everest, an ongoing effort using F* and Low* to verify and deploy secure components in the HTTPS ecosystem, including protocols such TLS and the cryptographic algorithms that underlie it

Tue 19 Jun

Displayed time zone: Eastern Time (US & Canada) change

14:00 - 15:40
Verified Low-Level Programming in F*PLDI Tutorials at Discovery C
14:00
1h40m
Other
Verified Low-Level Programming in F*
PLDI Tutorials
Jonathan Protzenko Microsoft Research, Redmond, Nikhil Swamy Microsoft Research, Tahina Ramananandro Microsoft Research, n.n.
16:10 - 17:35
Verified Low-Level Programming in F*PLDI Tutorials at Discovery C
16:10
85m
Other
Verified Low-Level Programming in F*
PLDI Tutorials
Jonathan Protzenko Microsoft Research, Redmond, Nikhil Swamy Microsoft Research, Tahina Ramananandro Microsoft Research, n.n.