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

[Peter Sewell]

There was a typo in the message title, sorry - as in the body, the
registration deadline is 31 August.

Peter


On Mon, 19 Aug 2024 at 16:33, Peter Sewell <Peter.Sewell at cl.cam.ac.uk>
wrote:

> 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!VgiSsbDuhlsxHtCxbaqCCvQcJ5EmcBHFn8jmyZI0Iz4uKSLmKOqmek6adD5b8OebiOoYD34uzVrD7c_raNlRtSOORmMebt3P_36-RW_u5w$ 
> 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/20240820/13b1c54d/attachment-0001.htm>