CPP 2024
Mon 15 - Tue 16 January 2024
London, United Kingdom
co-located with
POPL 2024
Toggle navigation
Attending
Venue: Institution of Engineering and Technology
Program
CPP Program
Your Program
Mon 15 Jan
Tue 16 Jan
Track/Call
Organization
CPP 2024 Committees
Track Committees
Organizing Committee
Program Committee
Steering Committee
Contributors
People Index
Search
Series
Series
CPP 2025
CPP 2024
CPP 2023
CPP 2022
CPP 2021
CPP 2020
CPP 2019
CPP 2018
CPP 2017
CPP 2016
Sign in
Sign up
POPL 2024
(
series
) /
CPP 2024 (
series
) /
Institution of Engineering and Technology
/
Room information: Mountbatten Exhibition
Venue
Institution of Engineering and Technology
Room name
Mountbatten Exhibition
Floor
2
Room Information
No extra information available
Program
Detailed Table
Session Timeline
Detailed Timeline
Program Display Configuration
Time Zone
The program is currently displayed in
(GMT) London
.
Use conference time zone: (GMT) London
Select other time zone
(GMT-12:00) AoE (Anywhere On Earth)
(GMT-11:00) Midway Island, Samoa
(GMT-10:00) Hawaii-Aleutian
(GMT-10:00) Hawaii
(GMT-09:30) Marquesas Islands
(GMT-09:00) Gambier Islands
(GMT-09:00) Alaska
(GMT-08:00) Tijuana, Baja California
(GMT-08:00) Pitcairn Islands
(GMT-08:00) Pacific Time (US & Canada)
(GMT-07:00) Mountain Time (US & Canada)
(GMT-06:00) Chihuahua, La Paz, Mazatlan
(GMT-07:00) Arizona
(GMT-06:00) Saskatchewan, Central America
(GMT-05:00) Guadalajara, Mexico City, Monterrey
(GMT-05:00) Easter Island
(GMT-06:00) Central Time (US & Canada)
(GMT-05:00) Eastern Time (US & Canada)
(GMT-05:00) Cuba
(GMT-05:00) Bogota, Lima, Quito, Rio Branco
(GMT-04:00) Caracas
(GMT-03:00) Santiago
(GMT-04:00) La Paz
(GMT-03:00) Faukland Islands
(GMT-04:00) Manaus, Amazonas, Brazil
(GMT-04:00) Atlantic Time (Goose Bay)
(GMT-04:00) Atlantic Time (Canada)
(GMT-03:30) Newfoundland
(GMT-03:00) UTC-3
(GMT-03:00) Montevideo
(GMT-03:00) Miquelon, St. Pierre
(GMT-03:00) Greenland
(GMT-03:00) Buenos Aires
(GMT-03:00) Brasilia, Distrito Federal, Brazil
(GMT-02:00) Mid-Atlantic
(GMT-01:00) Cape Verde Is.
(GMT-01:00) Azores
(UTC) Coordinated Universal Time
(GMT) Belfast
(GMT) Dublin
(GMT) Lisbon
(GMT) London
(GMT) Monrovia, Reykjavik
(GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
(GMT+01:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague
(GMT+01:00) Brussels, Copenhagen, Madrid, Paris
(GMT+01:00) West Central Africa
(GMT+02:00) Windhoek
(GMT+02:00) Athens
(GMT+02:00) Beirut
(GMT+02:00) Cairo
(GMT+02:00) Gaza
(GMT+02:00) Harare, Pretoria
(GMT+02:00) Jerusalem
(GMT+03:00) Minsk
(GMT+03:00) Syria
(GMT+03:00) Moscow, St. Petersburg, Volgograd
(GMT+03:00) Nairobi
(GMT+03:30) Tehran
(GMT+04:00) Abu Dhabi, Muscat
(GMT+04:00) Yerevan
(GMT+04:30) Kabul
(GMT+05:00) Ekaterinburg
(GMT+05:00) Tashkent
(GMT+05:30) Chennai, Kolkata, Mumbai, New Delhi
(GMT+05:45) Kathmandu
(GMT+06:00) Astana, Dhaka
(GMT+07:00) Novosibirsk
(GMT+06:30) Yangon (Rangoon)
(GMT+07:00) Bangkok, Hanoi, Jakarta
(GMT+07:00) Krasnoyarsk
(GMT+08:00) Beijing, Chongqing, Hong Kong, Urumqi
(GMT+08:00) Irkutsk, Ulaan Bataar
(GMT+08:00) Perth
(GMT+08:45) Eucla
(GMT+09:00) Osaka, Sapporo, Tokyo
(GMT+09:00) Seoul
(GMT+09:00) Yakutsk
(GMT+10:30) Adelaide
(GMT+09:30) Darwin
(GMT+10:00) Brisbane
(GMT+11:00) Hobart
(GMT+10:00) Vladivostok
(GMT+11:00) Lord Howe Island
(GMT+11:00) Solomon Is., New Caledonia
(GMT+11:00) Magadan
(GMT+12:00) Norfolk Island
(GMT+12:00) Anadyr, Kamchatka
(GMT+13:00) Auckland, Wellington
(GMT+12:00) Fiji, Kamchatka, Marshall Is.
(GMT+13:45) Chatham Islands
(GMT+13:00) Nuku'alofa
(GMT+14:00) Kiritimati
The GMT offsets shown reflect the offsets
at the moment of the conference
.
Time Band
By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.
Display full program
Specify a time band
-
Save
×
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 1
O'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
James Brotherston
10:07
22m
Talk
Verified Software at Scale
O'Hearn Fest
Philippa Gardner
Imperial College London
11:00 - 12:30
Session 2
O'Hearn Fest
at
Mountbatten Exhibition
Chair(s):
Hongseok Yang
KAIST; IBS
11:00
22m
Talk
Later Credits: A Case Study in the Unreasonable Effectiveness of Separation Logic
O'Hearn Fest
Derek Dreyer
MPI-SWS
11:22
22m
Talk
Bi-abductive adversarial program synthesis
O'Hearn Fest
Julien Vanegue
Bloomberg, USA
11:45
22m
Talk
CSL and relaxed memory
O'Hearn Fest
Stephen Brookes
CMU
12:07
22m
Talk
Is Peter Correct or Incorrect?
O'Hearn Fest
Patrick Cousot
14:00 - 15:30
Session 3
O'Hearn Fest
at
Mountbatten Exhibition
Chair(s):
Nick Benton
Meta
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
Patrice Godefroid
Lacework
16:00 - 17:30
Session 4
O'Hearn Fest
at
Mountbatten Exhibition
Chair(s):
Andy Adams-Moran
Meta
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
Nick Benton
Meta
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
Dino Distefano
Meta
Mon 15 Jan
Displayed time zone:
London
change
09:00 - 10:30
Morning Track 2
POPL TutorialFest
at
Mountbatten Exhibition
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
Morning Track 2
POPL TutorialFest
at
Mountbatten Exhibition
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
Afternoon Track 2
POPL TutorialFest
at
Mountbatten Exhibition
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
Afternoon Track 2
POPL TutorialFest
at
Mountbatten Exhibition
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
Opening
Incorrectness
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 Analysis
Incorrectness
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-properties
Incorrectness
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
Tobias Nießen
TU Wien
,
Georg Weissenbacher
TU Wien
DOI
Pre-print
16:00 - 17:30
Types
Incorrectness
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
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Mountbatten Exhibition
O'Hearn Fest
Session 1
O'Hearn Fest
Session 2
O'Hearn Fest
Session 3
O'Hearn Fest
Session 4
Mon 15 Jan
Displayed time zone:
London
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Mountbatten Exhibition
POPL TutorialFest
Morning Track 2
POPL TutorialFest
Morning Track 2
POPL TutorialFest
Afternoon Track 2
POPL TutorialFest
Afternoon Track 2
Tue 16 Jan
Displayed time zone:
London
change
Room
9:00
30
10:00
30
11:00
30
12:00
30
13:00
30
14:00
30
15:00
30
16:00
30
17:00
30
Mountbatten Exhibition
Incorrectness
Opening
Incorrectness
Logics and Program Analysis
Incorrectness
Concurrency, Security, & Hyper-properties
Incorrectness
Types
Sun 14 Jan
Displayed time zone:
London
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Mountbatten Exhibition
O'Hearn Fest
Introduction
09:00 - 09:22
O'Hearn Fest
Peter's early work on parametricity, and why it still matters to me
09:22 - 09:45
O'Hearn Fest
Strong vs. weak separating conjunction in CSL
09:45 - 10:07
O'Hearn Fest
Verified Software at Scale
10:07 - 10:30
O'Hearn Fest
Later Credits: A Case Study in the Unreasonable Effectiveness of Separa ...
11:00 - 11:22
O'Hearn Fest
Bi-abductive adversarial program synthesis
11:22 - 11:45
O'Hearn Fest
CSL and relaxed memory
11:45 - 12:07
O'Hearn Fest
Is Peter Correct or Incorrect?
12:07 - 12:30
O'Hearn Fest
Massive proofs for the masses
14:00 - 14:22
O'Hearn Fest
Designing Wait-free Weak Reference Counting
14:22 - 14:45
O'Hearn Fest
Elegance and generosity are scientific values - And other things I've l ...
14:45 - 15:07
O'Hearn Fest
Peter, the May and the Must, and Lacework
15:07 - 15:30
O'Hearn Fest
Working with Peter O'Hearn in academia and industry
16:00 - 16:22
O'Hearn Fest
Pete's Footprints
16:22 - 16:45
O'Hearn Fest
Symbolic Execution with Separating Decision Diagrams
16:45 - 17:07
O'Hearn Fest
With Peter from Theory to Engineering
17:07 - 17:30
Mon 15 Jan
Displayed time zone:
London
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
17:00
15
30
45
Mountbatten Exhibition
POPL TutorialFest
Pulse: Proof-oriented Programming in a Concurrent Separation Logic DSL ...
09:00 - 10:30
POPL TutorialFest
Pulse: Proof-oriented Programming in a Concurrent Separation Logic DSL ...
11:00 - 12:30
POPL TutorialFest
Cedar: A language for expressing fast, safe, and fine-grained authoriza ...
14:00 - 15:30
POPL TutorialFest
Cedar: A language for expressing fast, safe, and fine-grained authoriza ...
16:00 - 17:30
Tue 16 Jan
Displayed time zone:
London
change
Room
9:00
15
30
45
10:00
15
30
45
11:00
15
30
45
12:00
15
30
45
13:00
15
30
45
14:00
15
30
45
15:00
15
30
45
16:00
15
30
45
Mountbatten Exhibition
Incorrectness
Welcome
09:00 - 09:05
Incorrectness
My Journey to the Dark Side: Under-Approximation, Incorrectness, Proof
09:05 - 10:05
Incorrectness
A Comparison of Program Logics for (In)Correctness
10:05 - 10:27
Incorrectness
Unified Compositional Formal Methods: Exact Separation Logic and the Gi ...
11:00 - 11:22
Incorrectness
The Never-Ending Trace: An Under-Approximate Approach to Divergence Bugs
11:22 - 11:45
Incorrectness
Work in Progress: Modelling Incorrect Programs in the Open World with Dafny
11:45 - 12:07
Incorrectness
Hoare-Like Triples and Kleene Algebras with Top and Tests
12:07 - 12:30
Incorrectness
Quantitative Weakest Hyper Pre
14:00 - 14:22
A Reachability Logic for a Weak Memory Model with Promises
14:22 - 14:45
Incorrectness
Towards Temporal Adversarial Logic
14:45 - 15:07
Incorrectness
Finding counterexamples to ∀∃ hyperproperties
15:07 - 15:30
Incorrectness
Type-Based Incorrectness Reasoning
16:00 - 16:22
Incorrectness
Ill-Typed Programs Don't Evaluate
16:23 - 16:45
x
Sat 21 Dec 17:07