Live Verification in an Interactive Proof Assistant (PLDI 2024 - PLDI Research Papers)

Mon 24 - Fri 28 June 2024 Copenhagen, Denmark

Who

Samuel Gruetter, Viktor Fukala, Adam Chlipala

Track

PLDI 2024 PLDI Research Papers

Time Zone

The program is currently displayed in (GMT+02:00) Windhoek.

Use conference time zone: (GMT+02:00) WindhoekSelect other time zone

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 programSpecify a time band

Save

When

Thu 27 Jun 2024 11:40 - 12:00 at Finland / Norway - Formally Verified Chair(s): Peter Müller

DOI

https://doi.org/10.1145/3656439

Samuel Gruetter

Massachusetts Institute of Technology

Viktor Fukala

Massachusetts Institute of Technology

Adam Chlipala

Massachusetts Institute of Technology

United States

Time Zone

The program is currently displayed in (GMT+02:00) Windhoek.

Use conference time zone: (GMT+02:00) WindhoekSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

Display full programSpecify a time band

Save

Session Program

Thu 27 Jun
Displayed time zone: Windhoek change

10:40 - 12:20	Formally VerifiedPLDI Research Papers at Finland / Norway Chair(s): Peter Müller ETH Zurich

10:40 20m Talk		The Functional Essence of Imperative Binary Search Trees PLDI Research Papers Anton Lorenzen University of Edinburgh, Daan Leijen Microsoft Research, Wouter Swierstra Utrecht University, Netherlands, Sam Lindley University of Edinburgh DOI Pre-print
11:00 20m Talk		Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq PLDI Research Papers Simon Spies MPI-SWS, Lennard Gäher MPI-SWS, Michael Sammler MPI-SWS, Derek Dreyer MPI-SWS DOI Pre-print
11:20 20m Talk		Maximum Consensus Floating Point Solutions for Infeasible Low-Dimensional Linear Programs with Convex Hull as the Intermediate Representation PLDI Research Papers Mridul Aanjaneya Rutgers University, Santosh Nagarakatte Rutgers University DOI Pre-print
11:40 20m Talk		Live Verification in an Interactive Proof Assistant PLDI Research Papers Samuel Gruetter Massachusetts Institute of Technology, Viktor Fukala Massachusetts Institute of Technology, Adam Chlipala Massachusetts Institute of Technology DOI
12:00 20m Talk		Predictable Verification using Intrinsic Definitions PLDI Research Papers Adithya Murali University of Illinois at Urbana-Champaign, Cody Rivera University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign DOI