Verification under Intel-x86 with Persistency (PLDI 2024 - PLDI Research Papers) - PLDI 2024

Mon 24 - Fri 28 June 2024 Copenhagen, Denmark

Who

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, K Narayan Kumar, Prakash Saivasan

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

Wed 26 Jun 2024 14:20 - 14:40 at Iceland / Denmark - Formal Verification 1 Chair(s): Jeehoon Kang

DOI

https://doi.org/10.1145/3656425

Parosh Aziz Abdulla

Uppsala University, Sweden

Mohamed Faouzi Atig

Uppsala University, Sweden

Sweden

Ahmed Bouajjani

IRIF, Université Paris Diderot

France

K Narayan Kumar

Chennai Mathematical Institute

India

Prakash Saivasan

The Institute of Mathematical Sciences, India

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

Wed 26 Jun
Displayed time zone: Windhoek change

	13:40 - 15:20	Formal Verification 1PLDI Research Papers at Iceland / Denmark Chair(s): Jeehoon Kang KAIST

	13:40 20m Talk		Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language PLDI Research Papers Gaurav Parthasarathy ETH Zurich, Thibault Dardinier ETH Zurich, Benjamin Bonneau Verimag, Peter Müller ETH Zurich, Alexander J. Summers University of British Columbia DOI
	14:00 20m Talk		Verified Extraction from Coq to OCaml PLDI Research Papers Yannick Forster Inria, Matthieu Sozeau Inria, Nicolas Tabareau Inria DOI
	14:20 20m Talk		Verification under Intel-x86 with Persistency PLDI Research Papers Parosh Aziz Abdulla Uppsala University, Sweden, Mohamed Faouzi Atig Uppsala University, Sweden, Ahmed Bouajjani IRIF, Université Paris Diderot, K Narayan Kumar Chennai Mathematical Institute, Prakash Saivasan The Institute of Mathematical Sciences, India DOI
	14:40 20m Talk		RefinedRust: A Type System for High-Assurance Verification of Rust Programs PLDI Research Papers Lennard Gäher MPI-SWS, Michael Sammler MPI-SWS, Ralf Jung ETH Zurich, Robbert Krebbers Radboud University Nijmegen, Derek Dreyer MPI-SWS DOI
	15:00 20m Talk		Hyperblock Scheduling for Verified High-Level Synthesis PLDI Research Papers Yann Herklotz Imperial College London, John Wickerson Imperial College London DOI Pre-print File Attached