bacam
1
As part of an Isaac Newton Institute programme on Big Specification, a workshop is being organised on:
Big Specification: Specification, Proof, and Testing at Scale
Tentative schedule:
Monday 7 October
| Time |
Title |
| 9:30 - 10:00 |
registration |
| 10:00 - 10:05 |
Director’s Briefing |
| 10:05 - 10:15 |
Organiser’s Welcome - Peter Sewell |
| 10:15 - 11:00 |
Alasdair Reid: Engineering large, multipurpose microprocessor specifications (using the x86-64 architecture as a case study) |
| 11:00 - 11:30 |
break |
| 11:30 - 12:15 |
Anna Slobodova: Micro-architectural modelling and verification of an x86 micro-processor |
| 12:15 - 12.45 |
Alasdair Armstrong: ISA specification in Sail |
| 12.45 - 14:00 |
lunch |
| 14:00 - 14:45 |
Gregory Malecha: Verifying a Concurrent Hypervisor in C++ |
| 14:45 - 15:30 |
Michael Sammler: Specification and verification of multi-language programs in separation logic |
| 15:30 - 16:00 |
break |
| 16:00 - 16:45 |
Arthur Charguéraud: OptiTrust: Producing Trustworthy High-Performance Code via Source-to-Source Transformations |
| 17:00 - 18:00 |
Welcome Wine Reception |
Tuesday 8 October
| Time |
Title |
| 9:30 - 10:15 |
Benjamin Pierce: Verse: Specification, Testing, and Verification for the Working Software Engineer |
| 10:15 - 11:00 |
John Hughes: Towards requirements based testing of Cardano smart contracts |
| 11:00 - 11:30 |
break |
| 11:30 - 12:15 |
Jean-Christophe Filliâtre: Proofs on Inductive Predicates in Why3 |
| 12:15 - 12.45 |
Kayvan Memarian / Jean Pichon-Pharabod: Executable specification of a production hypervisor: hypercalls and TLB management discipline |
| 12.45 - 14:00 |
lunch |
| 14:00 - 14:45 |
Brian Campbell / Thomas Bauereiss / Angus Hammond: Reasoning above ISA specifications, for arbitrary and known code |
| 14:45 - 15:30 |
Dominique Devriese: Katamaran and Universal Contracts: Formalizing, verifying and applying ISA security guarantees |
| 15:30 - 16:00 |
break |
| 16:00 - 16:45 |
Gil Hur: TBD |
Wednesday 9 October
| Time |
Title |
| 9:30 - 10:15 |
Andreas Rossberg: Evolving a formal language standard |
| 10:15 - 11:00 |
Conrad Watt: Ever-Mechanising the Ever-Expanding WebAssembly specification |
| 11:00 - 11:30 |
break |
| 11:30 - 12:15 |
Amal Ahmed: Formally Specifying ABIs using Realistic Realizability |
| 12:15 - 12.45 |
TBD |
| 12.45 - 14:00 |
lunch |
| afternoon |
free |
| 19:30 - 22:00 |
formal dinner |
Thursday 10 October
| Time |
Title |
| 9:30 - 10:15 |
David Cock: Specifying “real” computers: cache coherence, cut+paste SoCs, and the de-facto Operating System |
| 10:15 - 11:00 |
Warren Hunt: An ACL2-based x86-ISA Specification |
| 11:00 - 11:30 |
break |
| 11:30 - 12:15 |
Viktor Vafeiadis: Scaling up the automated verification of concurrent programs |
| 12:15 - 12.45 |
Ben Simner: Arm relaxed systems semantics |
| 12.45 - 14:00 |
lunch |
| 14:00 - 14:45 |
Peter Müller: Proving Information Flow Security for Concurrent Programs |
| 14:45 - 15:30 |
Tobias Grosser: TBD |
| 15:30 - 16:00 |
break |
| 16:00 - 16:45 |
…short talks… |
Friday 11 October
| Time |
Title |
| 9:30 - 10:15 |
Ranjit Jhala: Trustworthy Just-In-Time Compilers with Symbolic Meta-Execution |
| 10:15 - 11:00 |
Nik Swamy: Retrofitting Verified Parsers in the Windows Kernel with AI |
| 11:00 - 11:30 |
break |
| 11:30 - 12:15 |
Nobuko Yoshida: Expressiveness and Separation on Mixed Choice Multiparty Session Types |
| 12:15 - 12.45 |
Christopher Pulte: CN specification, verification, and testing for systems C code |
| 12.45 - 14:00 |
lunch |
| 14:00 - 14:45 |
Jules Villard: TBD |
| 14:45 - 15:30 |
Anthony Fox: TBD |
| 15:30 - 16:00 |
break |