Big Specification: Specification, Proof, and Testing at Scale

Workshop theme

Computer programs can only be correct or incorrect relative to a specification of their behaviour. As a result, any form of program assurance -- be it testing, static analysis, or formal proof -- is only possible if we have at least a partial specification of the program's allowed behaviours.

Modern computer systems are built in layers, starting with instruction set architectures at the bottom layer up to operating systems and computer networks in the middle all the way up to applications like web browser at the very top -- and each and every one of these layers is incredibly complex. This creates a fundamental tension.

Assurance of an implementation of any layer of the software stack requires an accurate specification of it -- and those specifications can be incredibly massive. Working with such large specifications creates extremely difficult problems, ranging from the purely bureaucratic (how can editors update such specifications in such a way that they have confidence that all needed updates happen in sync), to engineering (tools such as model checkers and proof assistants can start crashing in the face of massive specs), to the scientific (how can we know that a large spec has the properties we hope it does).

Despite being difficulties, these difficulties are fundamentally good to have: the field has matured to the point where understanding how to write, maintain, and use large specifications is an important immediate problem, rather than a problem we hope to have in the future. This workshop gathers experts from across the spectrum of verification and assurance to share our experiences developing, using, and maintaining the kinds of complex specifications needed to engineer practical computer systems.

Applications for this workshop are now closed

Fees

Registration Only

Registration Package: £219
Student Registration Package: £169

The Registration Package includes admission to all seminars, lunches and refreshments on the days that lectures take place (Monday - Friday), wine reception and formal dinner, but does not include other meals or accommodation.

Accommodation Package

Limited funding support for accommodation may be available. To request this, please select the "accommodation package" in your application.

Unfortunately we do not have any accommodation to offer so all successful applicants will need to source and book their own accommodation.

Virtual Registration

Virtual Registration Package: £0

Virtual registration is free, and includes virtual admission to all seminars and does not include physical attendance, meals or accommodation.

Formal Dinner Only

Formal Dinner: £60

Participants on the Accommodation Package or Registration Package, including organisers and speakers, are automatically included in this event. For all remaining participants who would like to attend, such as programme participants, the above charge will apply.

Accommodation

Unfortunately we do not have any accommodation to offer so all successful applicants will need to source their own accommodation.

Limited funding support for accommodation may be available. To request this, please select the "accommodation package" in your application.

Local hotels and accommodation services:

The Institute accepts no responsibility for these services.

Meals

Lunch

Lunch will be served at Churchill College. Attendees will be provided with lunch vouchers for 2 courses and 1 drink. Timings will be confirmed with the timetable.

Evening Meal

Participants are free to make their own arrangements for dinner.

Formal Dinner

The Formal Dinner will be held at Selwyn College on Wednesday 9th October at 19:30.

Selwyn College was founded in 1882, and boasts beautiful landscaped gardens. The event is a tradition for INI participants and gives you a chance to socialise with your colleagues on a more personal level. It is not one to miss!

Timetable

Monday 7th October 2024
09:30 to 10:00	Registration	No Room Required
10:00 to 10:15	Director's Briefing and Organiser's Welcome	No Room Required
10:15 to 11:00	Alastair Reid Intel Engineering large, multipurpose microprocessor specifications (using the x86-64 architecture as a case study)	Room 1
11:00 to 11:30	Morning Coffee	No Room Required
11:30 to 12:15	Anna Slobodova Intel Micro-architectural modelling and verification of an x86 micro-processor	Room 1
12:15 to 12:45	Alasdair Armstrong University of Cambridge ISA specification in Sail	Room 1
12:45 to 14:00	Lunch at Churchill College	No Room Required
14:00 to 14:45	Gregory Malecha Bed Rock Systems Verifying a Concurrent Hypervisor in C++	Room 1
14:45 to 15:30	Michael Sammler ETH Zürich Specification and verification of multi-language programs in separation logic	Room 1
15:30 to 16:00	Afternoon Tea	No Room Required
16:00 to 16:45	Arthur Charguéraud INRIA OptiTrust: Producing Trustworthy High-Performance Code via Source-to-Source Transformation	Room 1
17:00 to 18:00	Welcome Wine Reception	No Room Required

Tuesday 8th October 2024
09:30 to 10:15	Benjamin Pierce University of Pennsylvania Verse: Specification, Testing, and Verification for the Working Software Engineer	Room 1
10:15 to 11:00	Robert John Muir Hughes Chalmers University of Technology Towards requirements based testing of Cardano smart contract	Room 1
11:00 to 11:30	Group Photo and Morning Coffee	No Room Required
11:30 to 12:15	Jean-Christophe Filliatre CNRS (Centre national de la recherche scientifique); Université Paris Saclay Proofs on Inductive Predicates in Why3	Room 1
12:15 to 12:45	Jean Pichon-Pharabod Aarhus Universitet ; Kayvan Memarian University of Cambridge Executable specification of a production hypervisor: hypercalls and TLB management discipline	Room 1
12:45 to 14:00	Lunch at Churchill College	No Room Required
14:00 to 14:45	Angus Hammond University of Cambridge ; Brian Campbell University of Edinburgh ; Thomas Bauereiss University of Cambridge Reasoning above ISA specifications, for arbitrary and known code	Room 1
14:45 to 15:30	Dominique Devriese Vrije Universiteit Brussel Katamaran and Universal Contracts: Formalizing, verifying and applying ISA security guarantees	Room 1
15:30 to 16:00	Afternoon Tea	No Room Required
16:00 to 16:45	Chung-Kil Hur Seoul National University Title TBC	Room 1

Wednesday 9th October 2024
09:30 to 10:15	Andreas Rossberg None / Other Evolving a formal language standard	Room 1
10:15 to 11:00	Conrad Watt Nanyang Technological University Ever-Mechanising the Ever-Expanding WebAssembly specification	Room 1
11:00 to 11:30	Morning Coffee	No Room Required
11:30 to 12:15	Amal Ahmed Northeastern University Formally Specifying ABIs using Realistic Realizability	Room 1
12:45 to 14:00	Lunch at Churchill College	No Room Required
19:30 to 22:00	Formal Dinner at Selwyn College	No Room Required

Thursday 10th October 2024
09:30 to 10:15	David Cock ETH Zürich Specifying "real" computers: cache coherence, cut+paste SoCs, and the de-facto Operating System	Room 1
10:15 to 11:00	Warren Hunt University of Texas at Austin An ACL2-based x86-ISA Specification	Room 1
11:00 to 11:30	Morning Coffee	No Room Required
11:30 to 12:15	Viktor Vafeiadis Max Planck Institute for Software Systems Scaling up the automated verification of concurrent programs	Room 1
12:15 to 12:45	Ben Simner University of Cambridge Arm relaxed systems semantics	Room 1
12:45 to 14:00	Lunch at Churchill College	No Room Required
14:00 to 14:45	Peter Müller ETH Zürich Proving Information Flow Security for Concurrent Programs	Room 1
14:45 to 15:30	Tobias Grosser University of Cambridge Title TBC	Room 1
15:30 to 16:00	Afternoon Tea	No Room Required

Friday 11th October 2024
09:30 to 10:15	Ranjit Jhala University of California, San Diego Trustworthy Just-In-Time Compilers with Symbolic Meta-Execution	Room 1
10:15 to 11:00	Nikhil Swamy Microsoft (USA) Retrofitting Verified Parsers in the Windows Kernel with AI	Room 1
11:00 to 11:30	Morning Coffee	No Room Required
11:30 to 12:15	Nobuko Yoshida University of Oxford Expressiveness and Separation on Mixed Choice Multiparty Session Types	Room 1
12:15 to 12:45	Christopher Pulte University of Cambridge CN specification, verification, and testing for systems C code	Room 1
12:45 to 14:00	Lunch at Churchill College	No Room Required
14:00 to 14:45	Jules Villard None / Other Title TBC	Room 1
15:30 to 16:00	Afternoon Tea	No Room Required

Organisers

Neel Krishnaswami University of Cambridge
Peter Sewell University of Cambridge
Natarajan Shankar SRI International

Speakers

Amal Ahmed Northeastern University
Alasdair Armstrong University of Cambridge
Thomas Bauereiss University of Cambridge
Brian Campbell University of Edinburgh
Arthur Charguéraud INRIA
David Cock ETH Zürich
Dominique Devriese Vrije Universiteit Brussel
Jean-Christophe Filliatre CNRS (Centre national de la recherche scientifique); Université Paris Saclay
Tobias Grosser University of Cambridge
Angus Hammond University of Cambridge
Robert John Muir Hughes Chalmers University of Technology
Warren Hunt University of Texas at Austin
Chung-Kil Hur Seoul National University
Ranjit Jhala University of California, San Diego
Gregory Malecha Bed Rock Systems
Kayvan Memarian University of Cambridge
Peter Müller ETH Zürich
Jean Pichon-Pharabod Aarhus Universitet
Benjamin Pierce University of Pennsylvania
Christopher Pulte University of Cambridge
Alastair Reid Intel
Andreas Rossberg None / Other
Michael Sammler ETH Zürich
Ben Simner University of Cambridge
Anna Slobodova Intel
Nikhil Swamy Microsoft (USA)
Viktor Vafeiadis Max Planck Institute for Software Systems
Jules Villard None / Other
Conrad Watt Nanyang Technological University
Nobuko Yoshida University of Oxford

Show All