{"id":49,"date":"2017-11-20T13:42:26","date_gmt":"2017-11-20T12:42:26","guid":{"rendered":"https:\/\/projects.lsv.ens-paris-saclay.fr\/epit18\/?page_id=49"},"modified":"2018-05-04T14:06:32","modified_gmt":"2018-05-04T13:06:32","slug":"program-verification-with-f","status":"publish","type":"page","link":"https:\/\/projects.lsv.ens-paris-saclay.fr\/epit18\/?page_id=49","title":{"rendered":"Program Verification with F*"},"content":{"rendered":"

Speaker<\/h2>\n

C\u0103t\u0103lin Hri\u0163cu<\/a> is a researcher of the Prosecco<\/a> team at Inria Paris<\/a>. He is one of the developers of the F*<\/a> programming language, and is leading a research effort in secure compilation<\/a> funded by an ERC starting grant. This course is thought together with\u00a0Antoine Delignat-Lavaud<\/a>, Danel Ahman<\/a>, and Victor Dumitrescu<\/a>.<\/p>\n

Abstract<\/h2>\n

F* is a general-purpose functional programming language with effects aimed at program verification. It puts together the automation of an SMT-backed deductive verification tool with the expressive power of a proof assistant based on dependent types. After verification, F* programs can be extracted to efficient OCaml, F#, or C code. This enables verifying the functional correctness and security of realistic applications, such as a verified HTTPS stack.<\/p>\n

This course will give an introduction to program verification in F* using simple examples and a few, even simpler exercises along the way. We will start with specifying and verifying purely-functional programs and then move to programs with side-effects such as divergence and mutable state. We will also cover F*’s support for\u00a0reasoning about monotonically evolving state and for adding extra monadic side-effects, which is for instance used to implement F*’s tactic system in F* itself. Finally, we will look a bit under the hood at how F* encodes verification conditions to the SMT and how it computes them in the first place using monads of predicate transformers, aka Dijkstra monads.<\/p>\n

References<\/h2>\n