Formal Verification with F* and Meta-F*

ECI 2019

1. Monday, July 22:
   • Overview of F* and Meta-F*, motivation from Project Everest
   • Basics of F*, refinement types ... (up to Slide 6)
2. Tuesday, July 23
   • Sections 1 -- 4 of the tutorial
   • More basics of F*, dependent types, termination proofs, intrinsic and extrinsic proofs (Slide 7 ... )
   • Live code sample
3. Wednesday, July 24
   • Effects in F*
   • Encoding F* to SMT (short)
   • Exercises
     • Exercise 1: memcpy (Dependences for Exercise 1)
     • Exercise 2: Machine integers, memcpy again
     • Exercise 2: Ring buffer 1
     • Exercise 3: Ring buffer 2
     • Exercise 4: Ring buffer 3
   • Vale: Verified Assembly Language for Everest
   • Efficient, extensible VC generation with typeclasses and normalization MiniValeSemantics.fst
4. Thursday, July 25
   • Slides
   • Intro.fst
   • Constructive.fst
   • Automation.fst
   • Hybrid.fst
5. Friday, July 26
   • Term.fst(as reference)
   • Metaprogramming.fst