|
|
|
09:30 to 10:00 |
Registration, Tea & Coffee |
|
|
|
|
|
|
|
10:00 to 10:10 |
Welcome and Introduction |
Jane Leeks (Newton 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), (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 (USA) ) |
|
|
|
|
|
|
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 |
|
|
|
|
