Program

Session 1:     9:00am – 10:30am

• 9:00am – Invited speaker: Adam Chlipala. Bedrock: A Clean-Slate Platform for Developing Verified Software Inside a Proof Assistant
• 10:00am – Emilio Jesús Gallego Arias, Olivier Hermant and Pierre Jouvelot. Verification of Faust Signal Processing Programs in Coq – Abstract

Break:     10:30am – 11am

Session 2:     11:00am – 12:30am

• 11:00am – Ilya Sergey, Aleksandar Nanevski and Anindya Banerjee. Towards Structured Mechanized Verification of Fine-Grained Concurrent Programs – Abstract
• 11:30am – Eric Mullen, Zachary Tatlock and Dan Grossman. Peek: A Formally Verified Peephole Optimization Framework for x86 – Abstract
• 12:00pm – Robbert Krebbers and Freek Wiedijk. Formalizing C in Coq – Abstract

Lunch:     12:30pm – 2:00pm

Session 3:     2:00pm – 3:30pm

• 2:00pm – Tobias Tebbi and Jason Gross. A Profiler for Ltac – Abstract
• 2:30pm – Gregory Malecha and Jesper Bengtson. Rtac: A Fully Reflective Tactic Language – Abstract
• 3:00pm – Zoe Paraskevopoulou, Catalin Hritcu, Maxime Dénès, Leonidas Lampropoulos and Benjamin C. Pierce. A Coq Framework For Verified Property-Based Testing – Abstract

Break:     3:30pm – 4:00pm

Session 4:     4:00pm – 5:30pm

• 4:00pm – Jason Gross. Coq Bug Minimizer – Abstract
• 4:30pm – Talk by the Coq developers