PLDI 2026
Mon 15 - Fri 19 June 2026
Boulder, Colorado, United States
Toggle navigation
Attending
Venue: Limelight Boulder
Registration
Sponsorship
Information for Presenters
Information for Session Chairs
Information for Attendees
PLDI Live Streams
Visa Letter
Lodging
Travel Information
Explore Boulder
Program
PLDI Program
Your Program
Mon 15 Jun
Tue 16 Jun
Wed 17 Jun
Thu 18 Jun
Fri 19 Jun
Tracks
PLDI 2026
PLDI Keynotes
PLDI Research Papers
PLDI Events
Diversity, Equity and Inclusion
PLDI Meetups
Student Research Competition
Tutorials
- ACT: End-to-End Compiler Infrastructure for Emerging AI Accelerators
- A guided tour through Oxidized OCaml
- Deep dive into the AWS Nitro Isolation Engine
- Implementing an Integrated Development Environment: a Quick Start Guide for PL Researchers
- Mechanized Specifications for Real-World Programming Languages
- Writing Performance-Portable Kernels Simplified with Helion
Research Artifacts
Workshops and Tutorials
Volunteering
Co-hosted Conferences
ISMM
Memory Management
LCTES
Programming Languages and Embedded Systems
Workshops
ARRAY
Array-oriented Programming
CP
Choreographic Programming
EGRAPHS
Equality Graphs
PAgE
Principles Of Agentic Engineering
PLMW @ PLDI
PL Mentoring Workshop
PROPL
Programming for the Planet
SOAP
State Of the Art in Program Analysis
Tom Ball @ Sixty
Tom Ball at 60
Organization
PLDI 2026 Committees
Organizing Committee
AV Committee
Track Committees
PLDI Research Papers
Student Research Competition
Research Artifacts
Contributors
People Index
Co-hosted Conferences
ISMM
Memory Management
Organizing Committee
Program Committee
LCTES
Programming Languages and Embedded Systems
Organizing Committee
Program Committee
Steering Committee
Workshops
ARRAY
Array-oriented Programming
Organizing Committee
Program Committee
CP
Choreographic Programming
Organizing Committee
Program Committee
EGRAPHS
Equality Graphs
Organizing Committee
Program Committee
PAgE
Principles Of Agentic Engineering
Organizing Committee
Program Committee
PLMW @ PLDI
PL Mentoring Workshop
Organizing Committee
PROPL
Programming for the Planet
Organizing Committee
Program Committee
SOAP
State Of the Art in Program Analysis
Organizing Committee
Keynote Speakers
Program Committee
Tom Ball @ Sixty
Organizing Committee
Program Committee
Search
Series
Series
PLDI 2027
PLDI 2026
PLDI 2025
PLDI 2024
PLDI 2023
PLDI 2022
PLDI 2021
PLDI 2020
PLDI 2019
PLDI 2018
PLDI 2017
PLDI 2016
PLDI 2015
Sign in
Sign up
PLDI 2026
(
series
) /
Limelight Boulder
/
Room information: Meadows B
Venue
Limelight Boulder
Room name
Meadows B
Floor
1
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-06:00) Mountain Time (US & Canada)
.
Use conference time zone: (GMT-06:00) Mountain Time (US & Canada)
Select other time zone
(GMT-12:00) AoE (Anywhere On Earth)
(GMT-11:00) Midway Island, Samoa
(GMT-09:00) Hawaii-Aleutian
(GMT-10:00) Hawaii
(GMT-09:30) Marquesas Islands
(GMT-09:00) Gambier Islands
(GMT-08:00) Alaska
(GMT-07:00) Tijuana, Baja California
(GMT-08:00) Pitcairn Islands
(GMT-07:00) Pacific Time (US & Canada)
(GMT-06:00) Mountain Time (US & Canada)
(GMT-06:00) Chihuahua, La Paz, Mazatlan
(GMT-07:00) Arizona
(GMT-06:00) Saskatchewan, Central America
(GMT-06:00) Guadalajara, Mexico City, Monterrey
(GMT-06:00) Easter Island
(GMT-05:00) Cancun
(GMT-05:00) Central Time (US & Canada)
(GMT-04:00) Eastern Time (US & Canada)
(GMT-04:00) Cuba
(GMT-05:00) Bogota, Lima, Quito, Rio Branco
(GMT-04:00) Caracas
(GMT-04:00) Santiago
(GMT-04:00) La Paz
(GMT-03:00) Faukland Islands
(GMT-04:00) Manaus, Amazonas, Brazil
(GMT-03:00) Atlantic Time (Goose Bay)
(GMT-03:00) Atlantic Time (Canada)
(GMT-02:30) Newfoundland
(GMT-03:00) UTC-3
(GMT-03:00) Montevideo
(GMT-02:00) Miquelon, St. Pierre
(GMT-02: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) Azores
(UTC) Coordinated Universal Time
(GMT+01:00) Belfast
(GMT+01:00) Dublin
(GMT+01:00) Lisbon
(GMT+01:00) London
(GMT) Monrovia, Reykjavik
(GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
(GMT+02:00) Belgrade, Bratislava, Budapest, Ljubljana, Prague
(GMT+02:00) Brussels, Copenhagen, Madrid, Paris
(GMT+01:00) West Central Africa
(GMT+02:00) Windhoek
(GMT+03:00) Athens
(GMT+03:00) Beirut
(GMT+02:00) Cairo
(GMT+03:00) Gaza
(GMT+02:00) Harare, Pretoria
(GMT+03: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+09:30) Adelaide
(GMT+09:30) Darwin
(GMT+10:00) Brisbane
(GMT+10:00) Hobart
(GMT+10:00) Vladivostok
(GMT+10:30) Lord Howe Island
(GMT+11:00) Solomon Is., New Caledonia
(GMT+11:00) Magadan
(GMT+11:00) Norfolk Island
(GMT+12:00) Anadyr, Kamchatka
(GMT+12:00) Auckland, Wellington
(GMT+12:00) Fiji, Kamchatka, Marshall Is.
(GMT+12: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
Mon 15 Jun
Displayed time zone:
Mountain Time (US & Canada)
change
09:00 - 10:10
Keynote
PAgE
at
Meadows B
Chair(s):
Shraddha Barke
Microsoft Research, Redmond
09:00
10m
Day closing
Opening remarks
PAgE
Shraddha Barke
Microsoft Research, Redmond
09:10
60m
Keynote
Formal Methods for Frontier AI Systems
PAgE
Gagandeep Singh
University of Illinois Urbana-Champaign
10:40 - 12:20
PAgE Session 1
PAgE
at
Meadows B
Chair(s):
Shraddha Barke
Microsoft Research, Redmond
10:40
20m
Talk
Agentic Code Reasoning
PAgE
Shubham Ugare
Meta
,
Satish Chandra
Meta Platforms, Inc.
Pre-print
11:00
20m
Talk
Towards Verified Code Reasoning by LLMs
PAgE
Meghana Aparna Sistla
Google DeepMind
,
Gogul Balakrishnan
Google
,
Patrick Rondon
Google
,
José Pablo Cambronero
Google, USA
,
Michele Tufano
Google
,
Satish Chandra
Meta Platforms, Inc.
11:20
20m
Talk
Testing, Credible Compilation, and Verification in the Axon Verified Compiler in Lean and Claude Code
Remote
PAgE
Martin C. Rinard
Massachusetts Institute of Technology
11:40
20m
Talk
The Next Frontier for AI-Generated Kernels: Correctness
PAgE
Guido Martínez
Microsoft Research
,
Tyler Sorensen
University of California at Santa Cruz
DOI
Pre-print
12:00
20m
Talk
Testing LLM-Generated Distributed Protocol Code
PAgE
Ankush Das
Boston University
,
Brendan Coyne
Boston University
13:40 - 15:20
PAgE Session 2
PAgE
at
Meadows B
13:40
20m
Talk
Combining Agentic AI and Lightweight Formal Methods To Find Bugs in a Production Hypervisor
PAgE
Hiroyuki Katsura
University of Cambridge
,
Kayvan Memarian
University of Cambridge
,
Peter Sewell
University of Cambridge
14:00
20m
Talk
From Workarounds to Root Causes: Experience Using Agentic Workflows to Debug Complex Browser GPU Compiler Stacks
PAgE
Abhijit Ramesh
UC Santa Cruz
,
Reese Levine
University of California at Santa Cruz
,
Tyler Sorensen
University of California at Santa Cruz
14:20
20m
Talk
Event-based Design Abstractions for Agent Harnesses
Recorded
PAgE
McCoy Becker
,
Matin Ghavami
Massachusetts Institute of Technology
,
Fabian Zaiser
Massachusetts Institute of Technology
,
Timothy J. O'Donnell
McGill University; Mila – Quebec AI Institute; CHI FRO; Canada CIFAR AI Chai, Mila
,
Martin C. Rinard
Massachusetts Institute of Technology
,
Joshua B. Tenenbaum
Massachusetts Institute of Technology
,
Vikash Mansinghka
Massachusetts Institute of Technology
14:40
20m
Talk
Lumos: Let there be Language Model System Certification
Remote
PAgE
Isha Chaudhary
,
Vedaant Jain
,
Prineet Parhar
,
Kavya Sachdeva
,
Avaljot Singh
University of Illinois Urbana-Champaign
,
Sayan Ranu
,
Gagandeep Singh
University of Illinois Urbana-Champaign
Pre-print
15:00
20m
Talk
Lazy Validation and Self-Healing for Agentic Programs
Remote
PAgE
Theodoros Tsampouris
Aristotle University of Thessaloniki
,
Eleftherios Ioannidis
Microsoft Research
,
Andreas Symeonidis
Aristotle University of Thessaloniki
15:50 - 17:00
PAgE Keynote
PAgE
at
Meadows B
15:50
60m
Keynote
Can Coding Agents Write Verifiably Correct Software?
Remote
PAgE
Shan Lu
Microsoft; University of Chicago
16:50
10m
Day closing
Closing Remarks
PAgE
Shraddha Barke
Microsoft Research, Redmond
Tue 16 Jun
Displayed time zone:
Mountain Time (US & Canada)
change
09:00 - 10:05
TomBall@60 Session 1
Tom Ball @ Sixty
at
Meadows B
Chair(s):
Shuvendu K. Lahiri
Microsoft Research
09:00
15m
Talk
Welcome and logistics
Tom Ball @ Sixty
Satish Chandra
Meta Platforms, Inc.
,
Shuvendu K. Lahiri
Microsoft Research
,
Mayur Naik
University of Pennsylvania
,
Byron Cook
Amazon
,
Madan Musuvathi
Microsoft Research
09:15
25m
Talk
Recollections from SLAM-ming with Tom
Tom Ball @ Sixty
Sriram Rajamani
Microsoft Research Indua
File Attached
09:40
25m
Talk
Tom and the evolution of abstraction
Tom Ball @ Sixty
Kenneth L. McMillan
University of Texas at Austin
File Attached
10:05
5m
Talk
Reminiscences from Madison and Naperville
Tom Ball @ Sixty
Satish Chandra
Meta Platforms, Inc.
10:40 - 12:20
TomBall@60 Session 2
Tom Ball @ Sixty
at
Meadows B
Chair(s):
Shuvendu K. Lahiri
Microsoft Research
10:40
25m
Talk
From Bebop to Constrained Horn Clauses
Tom Ball @ Sixty
Nikolaj Bjørner
Microsoft Research
File Attached
11:05
25m
Talk
Research in Three-Part Harmony
Tom Ball @ Sixty
Todd Millstein
University of California, Los Angeles
File Attached
11:30
25m
Talk
Riffing on some themes from Tom: Driver Verification, Testing, Abstraction & Theorem Proving
Tom Ball @ Sixty
Nikhil Swamy
Microsoft Research
File Attached
11:55
25m
Talk
The SLAM "GiveUp"
Tom Ball @ Sixty
Rahul Kumar
Amazon
File Attached
13:40 - 15:20
TomBall@60 Session 3
Tom Ball @ Sixty
at
Meadows B
Chair(s):
Satish Chandra
Meta Platforms, Inc.
13:40
25m
Talk
Ju-jitsu with Ball-Larus (& Melski-Reps) or "We will publish no algorithm before its time"
Tom Ball @ Sixty
Thomas Reps
University of Wisconsin-Madison
File Attached
14:05
25m
Talk
Having a Ball with Tom since 1994
Tom Ball @ Sixty
Patrice Godefroid
Microsoft, USA
File Attached
14:30
25m
Talk
The Question That Launched a Thousand Derivatives
Tom Ball @ Sixty
Margus Veanes
Microsoft Research
File Attached
14:55
25m
Talk
Tracing the Ball-istic Trajectory of My Research: From Randoop to FastF, Memory Models and Semantic Merging
Tom Ball @ Sixty
Shuvendu K. Lahiri
Microsoft Research
File Attached
15:50 - 17:30
TomBall@60 Session 4
Tom Ball @ Sixty
at
Meadows B
Chair(s):
Satish Chandra
Meta Platforms, Inc.
15:50
25m
Talk
Interdisciplinary Genius in the 21st Century: The Case of Tom Ball
Tom Ball @ Sixty
Mooly Sagiv
Certora, inc.
File Attached
16:15
13m
Talk
Profiling, not Slicing, is the Path to Success (pre-recorded video)
Tom Ball @ Sixty
James Larus
EPFL
Media Attached
16:28
12m
Talk
The BBC micro:bit revolution (pre-recorded video)
Tom Ball @ Sixty
Steve Hodges
Lancaster University, UK
16:40
30m
Talk
Paths Converge: Software Model Checking for the BBC micro:bit
Tom Ball @ Sixty
Thomas Ball
University of Washington (USA) and Lancaster University (UK)
File Attached
Mon 15 Jun
Displayed time zone:
Mountain Time (US & Canada)
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
Meadows B
PAgE
Keynote
PAgE
PAgE Session 1
PAgE
PAgE Session 2
PAgE
PAgE Keynote
Tue 16 Jun
Displayed time zone:
Mountain Time (US & Canada)
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
Meadows B
Tom Ball @ Sixty
TomBall@60 Session 1
Tom Ball @ Sixty
TomBall@60 Session 2
Tom Ball @ Sixty
TomBall@60 Session 3
Tom Ball @ Sixty
TomBall@60 Session 4
Mon 15 Jun
Displayed time zone:
Mountain Time (US & Canada)
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
Meadows B
PAgE
Opening remarks
09:00 - 09:10
PAgE
Formal Methods for Frontier AI Systems
09:10 - 10:10
PAgE
Agentic Code Reasoning
10:40 - 11:00
PAgE
Towards Verified Code Reasoning by LLMs
11:00 - 11:20
PAgE
Remote
Testing, Credible Compilation, and Verification in the Axon Verified Co ...
11:20 - 11:40
PAgE
The Next Frontier for AI-Generated Kernels: Correctness
11:40 - 12:00
PAgE
Testing LLM-Generated Distributed Protocol Code
12:00 - 12:20
PAgE
Combining Agentic AI and Lightweight Formal Methods To Find Bugs in a P ...
13:40 - 14:00
PAgE
From Workarounds to Root Causes: Experience Using Agentic Workflows to ...
14:00 - 14:20
PAgE
Recorded
Event-based Design Abstractions for Agent Harnesses
14:20 - 14:40
PAgE
Remote
Lumos: Let there be Language Model System Certification
14:40 - 15:00
PAgE
Remote
Lazy Validation and Self-Healing for Agentic Programs
15:00 - 15:20
PAgE
Remote
Can Coding Agents Write Verifiably Correct Software?
15:50 - 16:50
PAgE
Closing Remarks
16:50 - 17:00
Tue 16 Jun
Displayed time zone:
Mountain Time (US & Canada)
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
Meadows B
Tom Ball @ Sixty
Welcome and logistics
09:00 - 09:15
Tom Ball @ Sixty
Recollections from SLAM-ming with Tom
09:15 - 09:40
Tom Ball @ Sixty
Tom and the evolution of abstraction
09:40 - 10:05
Tom Ball @ Sixty
Reminiscences from Madison and Naperville
10:05 - 10:10
Tom Ball @ Sixty
From Bebop to Constrained Horn Clauses
10:40 - 11:05
Tom Ball @ Sixty
Research in Three-Part Harmony
11:05 - 11:30
Tom Ball @ Sixty
Riffing on some themes from Tom: Driver Verification, Testing, Abstract ...
11:30 - 11:55
Tom Ball @ Sixty
The SLAM "GiveUp"
11:55 - 12:20
Tom Ball @ Sixty
Ju-jitsu with Ball-Larus (& Melski-Reps) or "We will publish no algorit ...
13:40 - 14:05
Tom Ball @ Sixty
Having a Ball with Tom since 1994
14:05 - 14:30
Tom Ball @ Sixty
The Question That Launched a Thousand Derivatives
14:30 - 14:55
Tom Ball @ Sixty
Tracing the Ball-istic Trajectory of My Research: From Randoop to FastF ...
14:55 - 15:20
Tom Ball @ Sixty
Interdisciplinary Genius in the 21st Century: The Case of Tom Ball
15:50 - 16:15
Tom Ball @ Sixty
Profiling, not Slicing, is the Path to Success (pre-recorded video)
16:15 - 16:28
Tom Ball @ Sixty
The BBC micro:bit revolution (pre-recorded video)
16:28 - 16:40
Tom Ball @ Sixty
Paths Converge: Software Model Checking for the BBC micro:bit
16:40 - 17:10
x
Fri 24 Jul 22:45