<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!Q96u0guBe-Kh3K88iVkiK3l7J0HYkNv55JrkbCQ9P5nBLZPLrqAZFbejpRAD_rztAd1GTN4_7ah_rhKnToj1hRlw1S3XWdMb1rkHJIZ4bQ$">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>