<div dir="ltr"><div>There was a typo in the message title, sorry - as in the body, the registration deadline is 31 August.</div><div><br></div><div>Peter</div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Mon, 19 Aug 2024 at 16:33, Peter Sewell <<a href="mailto:Peter.Sewell@cl.cam.ac.uk">Peter.Sewell@cl.cam.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">As part of an Isaac Newton Institute programme on Big Specification,<br>we're having a workshop<br><br> Big Specification: Specification, Proof, and Testing at Scale<br><br>on 7-11 October 2024, at the Isaac Newton Institute, Cambridge, UK<br><br>Register at <a href="https://urldefense.com/v3/__https://www.newton.ac.uk/event/bspw01/__;!!IBzWLUs!VgiSsbDuhlsxHtCxbaqCCvQcJ5EmcBHFn8jmyZI0Iz4uKSLmKOqmek6adD5b8OebiOoYD34uzVrD7c_raNlRtSOORmMebt3P_36-RW_u5w$" target="_blank">https://www.newton.ac.uk/event/bspw01/</a><br>Deadline: 31 Aug 2024<br><br><br>Tentative schedule:<br><br>Monday 7 October<br><br> 9:30 - 10:00 registration<br>10:00 - 10:05 Director's Briefing<br>10:05 - 10:15 Organiser's Welcome - Peter Sewell<br>10:15 - 11:00 Alasdair Reid: Engineering large, multipurpose microprocessor specifications (using the x86-64 architecture as a case study)<br>11:00 - 11:30 break<br>11:30 - 12:15 Anna Slobodova: Micro-architectural modelling and verification of an x86 micro-processor<br>12:15 - 12.45 Alasdair Armstrong: ISA specification in Sail<br>12.45 - 14:00 lunch<br>14:00 - 14:45 Gregory Malecha: Verifying a Concurrent Hypervisor in C++<br>14:45 - 15:30 Michael Sammler: Specification and verification of multi-language programs in separation logic<br>15:30 - 16:00 break<br>16:00 - 16:45 Arthur Charguéraud: OptiTrust: Producing Trustworthy High-Performance Code via Source-to-Source Transformations<br>17:00 - 18:00 Welcome Wine Reception<br> <br>Tuesday 8 October<br> <br> 9:30 - 10:15 Benjamin Pierce: Verse: Specification, Testing, and Verification for the Working Software Engineer<br>10:15 - 11:00 John Hughes: Towards requirements based testing of Cardano smart contracts<br>11:00 - 11:30 break<br>11:30 - 12:15 Jean-Christophe Filliâtre: Proofs on Inductive Predicates in Why3<br>12:15 - 12.45 Kayvan Memarian / Jean Pichon-Pharabod: Executable specification of a production hypervisor: hypercalls and TLB management discipline<br>12.45 - 14:00 lunch<br>14:00 - 14:45 Brian Campbell / Thomas Bauereiss / Angus Hammond: Reasoning above ISA specifications, for arbitrary and known code<br>14:45 - 15:30 Dominique Devriese: Katamaran and Universal Contracts: Formalizing, verifying and applying ISA security guarantees<br>15:30 - 16:00 break<br>16:00 - 16:45 Gil Hur: TBD<br> <br>Wednesday 9 October<br> <br> 9:30 - 10:15 Andreas Rossberg: Evolving a formal language standard<br>10:15 - 11:00 Conrad Watt: Ever-Mechanising the Ever-Expanding WebAssembly specification<br>11:00 - 11:30 break<br>11:30 - 12:15 Amal Ahmed: Formally Specifying ABIs using Realistic Realizability<br>12:15 - 12.45 TBD <br>12.45 - 14:00 lunch<br>afternoon free <br>19:30 - 22:00 formal dinner<br> <br>Thursday 10 October<br> <br> 9:30 - 10:15 David Cock: Specifying "real" computers: cache coherence, cut+paste SoCs, and the de-facto Operating System<br>10:15 - 11:00 Warren Hunt: An ACL2-based x86-ISA Specification<br>11:00 - 11:30 break<br>11:30 - 12:15 Viktor Vafeiadis: Scaling up the automated verification of concurrent programs<br>12:15 - 12.45 Ben Simner: Arm relaxed systems semantics<br>12.45 - 14:00 lunch<br>14:00 - 14:45 Peter Müller: Proving Information Flow Security for Concurrent Programs<br>14:45 - 15:30 Tobias Grosser: TBD<br>15:30 - 16:00 break<br>16:00 - 16:45 ...short talks...<br> <br>Friday 11 October<br> <br> 9:30 - 10:15 Ranjit Jhala: Trustworthy Just-In-Time Compilers with Symbolic Meta-Execution<br>10:15 - 11:00 Nik Swamy: Retrofitting Verified Parsers in the Windows Kernel with AI<br>11:00 - 11:30 break<br>11:30 - 12:15 Nobuko Yoshida: Expressiveness and Separation on Mixed Choice Multiparty Session Types<br>12:15 - 12.45 Christopher Pulte: CN specification, verification, and testing for systems C code<br>12.45 - 14:00 lunch<br>14:00 - 14:45 Jules Villard: TBD<br>14:45 - 15:30 Anthony Fox: TBD<br>15:30 - 16:00 break<br><br><br></div>
</blockquote></div>