Predictable Verification using Intrinsic Definitions (PLDI 2024 - PLDI Research Papers)

Mon 24 - Fri 28 June 2024 Copenhagen, Denmark

Who

Adithya Murali, Cody Rivera, P. Madhusudan

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 12:00 - 12:20 at Finland / Norway - Formally Verified Chair(s): Peter Müller

DOI

https://doi.org/10.1145/3656450

Adithya Murali

University of Illinois at Urbana-Champaign

United States

Cody Rivera

University of Illinois at Urbana-Champaign

P. Madhusudan

University of Illinois at Urbana-Champaign

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