Monday, June 6th

• Morning sessions
  Andrew Appel (DeepSpec): Overview of DeepSpec
  Mitra Basu (National Science Foundation): NSF persepctive on DeepSpec
  Joe Kiniry (Galois): Formal Methods at Galois and Free & Fair
  Stephanie Weirich (DeepSpec): Core Haskell
  Hendrik Tews (FireEye): Formal Methods at FireEye - Current Project and Challenges
  Zhong Shao: Hypervisor/OS research in DeepSpec
  David Cok (Grammatech): Verification tools resulting from a project with NASA
  
• Afternoon sessions
  Lennart Beringer (DeepSpec): Verification of crypto primitives
  Adam Langley (Google): Crypto-landscape at Google
  Alley Stoughton (IMDEA): Applying Theoretical Crypto's Real/Ideal Paradigm to the Security of Ordinary Programs
  Christian Ferdinand (AbsInt): AbsInt's verification tools and ComPCert plans
  Richard Lethin (Reservoir Labs): Introduction to Rreservoir Labs
  Benjamin Pierce (DeepSpec): Quickchick - specification-based testing
  John Hughes (Chalmers Univ $amp; QuviQ): QuviQ
  Coq team (INRIA): Coq Consortium & and future plans for Coq

Tuesday, June 7th

• Morning sessions
  Adam Chlipala (DeepSpec): Processor Verification in DeepSpec
  Da Chuang & Sharad Chole (Cisco): Zero Time - Formal Driven Design Methodology
  Arvind (MIT): Formal Specification of RISC-V Systems Instructions
  Nick Benton & Chris Hawblitzel (Microsoft Research): Everest and other verification projects at MSR
  Steve Zdancewic (DeepSpec): Vellum: LLVM research in DeepSpec
  Nuno Lopes (Microsoft Research): Wish-list for DeepSpec-related technologies
  Andrew Appel (DeepSpec): Verified Software Toolchain: Verifiable C, CompCert, & concurrency
  Veronique Benzaken & Evelyne Contejean (LRI - CNRS - Universite Paris Sud): DataCert - Data Centri Systems Deep Specification
  
• Afternoon Sessions
  Peter Sewell (Cambridge): Rigorous Engineering for Mainstream Systems (REMS)
  Alastair Reid (ARM): Trustworthy Specifications of ARM System Level Architecture
  Benjamin Pierce (DeepSpec): Education efforts
  Michael Soegtrop (Intel): Automating Software Foundations, and formal methods at Intel Munich
  

Wednesday, June 8th

• Morning sessions
  Coq consortium (incl. Pierre-Marie Pedrot: Ltac 2.0)
  Gil Hur (Seoul National University): Weak Memory Model
  William Mansky (Univ. of Pennsylvania): Verifying Dynamic Race Detection
  Newman Wu (Yale): Toward Compositional Verification of Interruptible OS Kernels and Device Drivers
  Alastair Reid (ARM): End-to-End Verification of ARM Processors with ISA-Formal
  Tahina Ramananandro (Reservoir Labs): VCFloat: towards deep specifications for numerical software
  Gregory Malecha (Univ. of California at San Diego): MirrorCore: Quickly Building Fast Automation
  Valentin Robert (Univ. of California at San Diego): PeaCoq
  Mohsen Lesani (MIT): Certified Composable Transactions
  
• Afternoon sessions
  Robbert Krebbers (Aarhus Univ.): Interactive higher-order separation logic proofs in Coq
  Kenneth Roe (John-Hopkins-Univ.): CoqPIE
  Abishek Anand (Cornell): ROSCoq: Robots powered by constructive reals
  Michael Soegtrop (Intel Munich): Automating Software Foundations
  Gang Tan (Lehigh Univ.): Bidirectional Grammars for Machine-Code Decoding and Encoding
  Petar Maksimovic (Imperial College): JavaScript, Concurrency at Imperial
  Santosh Nagarakatte (Rutgers Univ.): Verifying LLVM Floating Point Optimizations with Alive-FP