# Big Specification workshop at the Newton Institute

**URL:** <https://discourse.rocq-prover.org/t/big-specification-workshop-at-the-newton-institute/2399>\
**Category:** Announcements\
**Created:** [August 19, 2024, 4:25pm UTC](https://discourse.rocq-prover.org/t/big-specification-workshop-at-the-newton-institute/2399 "2024-08-19T16:25:18Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![bacam](https://avatars.discourse-cdn.com/v4/letter/b/e8c25b/32.png) [@bacam](https://discourse.rocq-prover.org/u/bacam)\
**Post date:** [August 19, 2024, 4:25pm UTC](https://discourse.rocq-prover.org/t/big-specification-workshop-at-the-newton-institute/2399/1 "2024-08-19T16:25:18Z")

</div>

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**

- Date: 7-11 October 2024
- Location: the Isaac Newton Institute, Cambridge, UK
- Register at: [https://www.newton.ac.uk/event/bspw01/](https://www.newton.ac.uk/event/bspw01/)
- Deadline: 31 Aug 2024

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 |