skip to content



19th July 2017
09:30 to 10:00 Registration, Tea & Coffee
10:00 to 10:10 Welcome and Introduction Jane Leeks (Turing Gateway to Mathematics)
Session 1: Big Proof Foundations and Development
10:10 to 10:45 Can Machines Think Like Humans? Mateja Jamnik (University of Cambridge)
10:45 to 11:20 Trustworthy Software Specification Philippa Gardner (Imperial College London)
11:20 to 11:40 Tea & Coffee
11:40 to 12:15 At-scale Formal Verification for Industrial Semiconductor Designs Tom Melham (University of Oxford)
12:15 to 12:50 New Challenges with Large Proofs in the wake of the Formal Proof of the Kepler Conjecture Thomas Hales (University of Pittsburgh)
12:50 to 13:00 Questions
13:00 to 14:00 Lunch
Session 2: Big Proof Achievements and Applications
14:00 to 14:35 Challenges in Analysing Virtualisation Stacks Michael Tautschnig (Queen Mary University of London)
14:35 to 15:05 Bringing Big Verification to Big Finance Grant Passmore (Aesthetic Integration Ltd)
15:05 to 15:25 Tea & Coffee
15:25 to 16:00 From Z3 to Lean, Efficient Verification Leonardo de Moura (Microsoft)
16:00 to 16:35 Deep Static Analysis at Facebook Speed and Scale Jules Villard (Facebook Research)
16:35 to 17:00 Panel Discussion and Wrap-Up - Big Proof Outlook and Future Challenges
17:00 to 18:00 Drinks Reception & Networking