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

pldi-2018-PLDI-Tutorials
14:00 - 15:40: PLDI Tutorials - Verified Low-Level Programming in F* at Discovery C
pldi-2018-PLDI-Tutorials14:00 - 15:40
Other
Jonathan ProtzenkoMicrosoft Research, Redmond, Nikhil SwamyMicrosoft Research, Tahina RamananandroMicrosoft Research, n.n.
pldi-2018-PLDI-Tutorials
16:10 - 17:35: PLDI Tutorials - Verified Low-Level Programming in F* at Discovery C
pldi-2018-PLDI-Tutorials16:10 - 17:35
Other
Jonathan ProtzenkoMicrosoft Research, Redmond, Nikhil SwamyMicrosoft Research, Tahina RamananandroMicrosoft Research, n.n.