Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (PLDI 2024 - PLDI Research Papers) - PLDI 2024

Mon 24 - Fri 28 June 2024 Copenhagen, Denmark

Who

Thibault Dardinier, Peter Müller

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

When

Thu 27 Jun 2024 14:00 - 14:20 at Finland / Norway - Formal Verification 2 Chair(s): Clément Pit-Claudel

DOI

https://doi.org/10.1145/3656437

Thibault Dardinier

ETH Zurich

Switzerland

Peter Müller

ETH Zurich

Switzerland

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

Session Program

Thu 27 Jun
Displayed time zone: Windhoek change

	13:40 - 14:40	Formal Verification 2PLDI Research Papers at Finland / Norway Chair(s): Clément Pit-Claudel EPFL

	13:40 20m Talk		Mechanised Hypersafety Proofs about Structured Data PLDI Research Papers Vladimir Gladshtein National University of Singapore, Qiyuan Zhao National University of Singapore, Willow Ahrens Massachusetts Institute of Technology, Saman Amarasinghe Massachusetts Institute of Technology, Ilya Sergey National University of Singapore DOI Pre-print
	14:00 20m Talk		Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties PLDI Research Papers Thibault Dardinier ETH Zurich, Peter Müller ETH Zurich DOI
	14:20 20m Talk		A HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite Automata PLDI Research Papers Zhe Zhou Purdue University, Qianchuan Ye Purdue University, Benjamin Delaware Purdue University, Suresh Jagannathan Purdue University DOI