Monday, June 18th

• Morning sessions
  

  The Science of Deep Specification
  Andrew Appel (Princeton)

  CakeML: from functions to machine code with proof all the way
  Magnus O. Myreen (Chalmers University of Technology, Sweden)

  Vellvm - Modular Semantics via Interaction Trees
  Steve Zdancewic (University of Pennsylvania)

  Crellvm
  Chung-Kil Hur (Seoul National University)

• Afternoon sessions
  

  Verifiable C, a logic and system for proving C programs correct
  Qinxiang Cao (Princeton)

  Progress Report on the DeepSpec Web Server
  Benjamin C. Pierce (University of Pennsylvania)

  QuickChick: Random Testing in Coq
  Leonidas Lampropoulos (University of Pennsylvania)

  Real-Time CertiKOS: A Step Toward Resource Adaptive Certified OS Kernels
  Zhong Shao (Yale University)

  Verification Around the Hardware-Software Interface: Instruction Set, Processors, and Side Channels
  Adam Chlipala (Massachusetts Institute of Technology, USA)

  Using Kami in the field - experiences integrating Kami into SiFive's Chisel/Scala-based design flow
  Muralidaran Vijayaraghavan (SiFive)

Tuesday, June 19th

• Morning sessions
  

  Modularity for Decidability: Implementing and Semi-Automatically Verifying Distributed Systems
  Mooly Sagiv (Tel Aviv University)

  Automation for High-Assurance Cryptography, for Primitives and Protocols
  Andres Erbsen (Massachusetts Institute of Technology, USA)

  Towards a formal semantics for GHC Core
  Stephanie Weirich (University of Pennsylvania, USA)

  Debugging Debug Information and Beyond
  Francesco Zappa Nardelli (Inria)

• Afternoon Sessions
  

  Multicore and Multithreaded Linking for Concurrent CertiKOS
  Jieung Kim (Yale University)

  Verifying seL4 towards Concurrency
  Thomas Sewell (University of New South Wales)

  Specifying and Verifying Concurrent Programs with Ghost State
  William Mansky (Princeton University)

  5-minute Lightning Talks
  

  • Simplicity for Smart Contracts
    Russell O'Connor (blockstream.com)
  • Machine-Verified Machine Learning
    Gordon Stewart (Ohio University)
  • Verification of Union-Find in C
    Shengyi Wang (Princeton University)
  • Narcissus: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats
    Clément Pit-Claudel (Massachusetts Institute of Technology)
  • LLVM's IR and Call-By-Push-Value Lambda Calculus
    Yannick Zakowski (University of Pennsylvania)
  • A Formal Equational Theory for Call-By-Push-Value
    Christine Rizkallah (University of New South Wales)
  • Serializability for Distributed Protocols
    Joonwon Choi (Massachusetts Institute of Technology)
  • A Quick Hack to ask any SMT Solver if my Coq Goal is True
    Sam Gruetter (Massachusetts Institute of Technology)