The Coq mailing list

[Peter Sewell <Peter.Sewell AT cl.cam.ac.uk>]

As part of an Isaac Newton Institute programme on Big Specification,
we're having a workshop

   Big Specification: Specification, Proof, and Testing at Scale

on 7-11 October 2024, at the Isaac Newton Institute, Cambridge, UK

Register at https://www.newton.ac.uk/event/bspw01/
Deadline: 31 Aug 2024


Tentative schedule:

Monday 7 October

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