[TYPES/announce] Workshop on Big Specification (Registration open until 31 Oct)

[Peter Sewell]

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://urldefense.com/v3/__https://www.newton.ac.uk/event/bspw01/__;!!IBzWLUs!Q96u0guBe-Kh3K88iVkiK3l7J0HYkNv55JrkbCQ9P5nBLZPLrqAZFbejpRAD_rztAd1GTN4_7ah_rhKnToj1hRlw1S3XWdMb1rkHJIZ4bQ$ 
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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20240819/9b9e67e8/attachment-0001.htm>