N40AI 2024
Sat 20 Jan 2024 London, United Kingdom
co-located with POPL 2024
VenueInstitution of Engineering and Technology
Room nameMountbatten Exhibition
Floor2
Room InformationNo extra information available
Program

You're viewing the program in a time zone which is different from your device's time zone change time zone

Sun 14 Jan

Displayed time zone: London change

09:00 - 10:30
Session 1O'Hearn Fest at Mountbatten Exhibition
Chair(s): Matthew J. Parkinson Microsoft Azure Research
09:00
22m
Talk
Introduction
O'Hearn Fest
Azalea Raad Imperial College London, Jules Villard Meta
09:22
22m
Talk
Peter's early work on parametricity, and why it still matters to me
O'Hearn Fest
Hongseok Yang KAIST; IBS
09:45
22m
Talk
Strong vs. weak separating conjunction in CSL
O'Hearn Fest
10:07
22m
Talk
Verified Software at Scale
O'Hearn Fest
Philippa Gardner Imperial College London
14:00 - 15:30
14:00
22m
Talk
Massive proofs for the masses
O'Hearn Fest
Byron Cook Amazon
14:22
22m
Talk
Designing Wait-free Weak Reference Counting
O'Hearn Fest
Matthew J. Parkinson Microsoft Azure Research
14:45
22m
Talk
Elegance and generosity are scientific values - And other things I've learned from Peter
O'Hearn Fest
Jade Alglave Arm and University College London
15:07
22m
Talk
Peter, the May and the Must, and Lacework
O'Hearn Fest
16:00 - 17:30
16:00
22m
Talk
Working with Peter O'Hearn in academia and industry
O'Hearn Fest
Mark Harman Meta Platforms, Inc. and UCL
16:22
22m
Talk
Pete's Footprints
O'Hearn Fest
16:45
22m
Talk
Symbolic Execution with Separating Decision Diagrams
O'Hearn Fest
Josh Berdine SkipLabs
17:07
22m
Talk
With Peter from Theory to Engineering
O'Hearn Fest

Mon 15 Jan

Displayed time zone: London change

09:00 - 10:30
09:00
90m
Tutorial
Pulse: Proof-oriented Programming in a Concurrent Separation Logic DSL in F*
POPL TutorialFest
Thibault Dardinier ETH Zurich, Megan Frisella Brown University, Guido Martínez Microsoft Research, Tahina Ramananandro Microsoft Research, Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research
11:00 - 12:30
11:00
90m
Tutorial
Pulse: Proof-oriented Programming in a Concurrent Separation Logic DSL in F*
POPL TutorialFest
Thibault Dardinier ETH Zurich, Megan Frisella Brown University, Guido Martínez Microsoft Research, Tahina Ramananandro Microsoft Research, Aseem Rastogi Microsoft Research, Nikhil Swamy Microsoft Research
14:00 - 15:30
14:00
90m
Talk
Cedar: A language for expressing fast, safe, and fine-grained authorization policies
POPL TutorialFest
Michael Hicks Amazon Web Services and the University of Maryland
16:00 - 17:30
16:00
90m
Talk
Cedar: A language for expressing fast, safe, and fine-grained authorization policies
POPL TutorialFest
Michael Hicks Amazon Web Services and the University of Maryland

Tue 16 Jan

Displayed time zone: London change

09:00 - 10:30
OpeningIncorrectness at Mountbatten Exhibition
Chair(s): Noam Zilberstein Cornell University
09:00
5m
Day opening
Welcome
Incorrectness
Noam Zilberstein Cornell University, Azalea Raad Imperial College London
09:05
60m
Keynote
My Journey to the Dark Side: Under-Approximation, Incorrectness, Proof
Incorrectness
Peter W. O'Hearn Lacework; University College London
10:05
22m
Talk
A Comparison of Program Logics for (In)Correctness
Incorrectness
Flavio Ascari University of Pisa
Pre-print File Attached
11:00 - 12:30
Logics and Program AnalysisIncorrectness at Mountbatten Exhibition
Chair(s): Noam Zilberstein Cornell University
11:00
22m
Talk
Unified Compositional Formal Methods: Exact Separation Logic and the Gillian Platform for Correctness and Incorrectness Reasoning
Incorrectness
Andreas Lööw Imperial College London, Daniele Nantes-Sobrinho Imperial College London, Sacha-Élie Ayoun Imperial College London, Nat Karmios Imperial College London, Seung Hoon Park Imperial College London, Petar Maksimović Imperial College London, UK, Philippa Gardner Imperial College London
Pre-print
11:22
22m
Talk
The Never-Ending Trace: An Under-Approximate Approach to Divergence Bugs
Incorrectness
Caroline Cronjäger Vrije Universiteit Amsterdam
Pre-print
11:45
22m
Talk
Work in Progress: Modelling Incorrect Programs in the Open World with Dafny
Incorrectness
James Noble Creative Research & Programming, Tobias Wrigstad Uppsala University, Susan Eisenbach Imperial College London
File Attached
12:07
22m
Talk
Hoare-Like Triples and Kleene Algebras with Top and Tests
Incorrectness
Lena Verscht Saarland University, Saarland Informatics Campus, Benjamin Lucien Kaminski Saarland University; University College London
Pre-print File Attached
14:00 - 15:30
Concurrency, Security, & Hyper-propertiesIncorrectness at Mountbatten Exhibition
Chair(s): Azalea Raad Imperial College London
14:00
22m
Talk
Quantitative Weakest Hyper Pre
Incorrectness
Linpeng Zhang University College London, Benjamin Lucien Kaminski Saarland University; University College London
File Attached
14:22
23m
Talk
A Reachability Logic for a Weak Memory Model with Promises
Incorrectness
Lara Bargmann University of Oldenburg, Brijesh Dongol University of Surrey, Heike Wehrheim University of Oldenburg
File Attached
14:45
22m
Talk
Towards Temporal Adversarial Logic
Incorrectness
Julien Vanegue Bloomberg, USA
15:07
22m
Talk
Finding counterexamples to ∀∃ hyperproperties
Incorrectness
DOI Pre-print
16:00 - 17:30
TypesIncorrectness at Mountbatten Exhibition
Chair(s): Azalea Raad Imperial College London
16:00
22m
Talk
Type-Based Incorrectness Reasoning
Incorrectness
Zhe Zhou Purdue University, Benjamin Delaware Purdue University, Suresh Jagannathan Purdue University
16:23
22m
Talk
Ill-Typed Programs Don't Evaluate
Incorrectness
Steven Ramsay University of Bristol, Charlie Walpole University of Bristol

Sun 14 Jan

Displayed time zone: London change