Verifying a C implementation of Derecho's coordination mechanism using VST and Coq (NASA Formal Methods 2024 - NFM 2024)

Who

Ramana Nagasamudram, Lennart Beringer, Ken Birman, Mae Milano, David Naumann

Track

NASA Formal Methods 2024 NFM

Time Zone

The program is currently displayed in (GMT-07:00) Pacific Time (US & Canada).

Use conference time zone: (GMT-07:00) Pacific Time (US & Canada)Select 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

Tue 4 Jun 2024 14:25 - 14:50 at Ballroom - FM for Program Analysis and Verification Chair(s): Douglas Smith

Ramana Nagasamudram

Stevens Institute of Technology

United States

Lennart Beringer

Princeton University

United States

Ken Birman

Cornell University

United States

Mae Milano

Princeton University

United States

David Naumann

Stevens Institute of Technology

United States

Time Zone

The program is currently displayed in (GMT-07:00) Pacific Time (US & Canada).

Use conference time zone: (GMT-07:00) Pacific Time (US & Canada)Select 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

Tue 4 Jun
Displayed time zone: Pacific Time (US & Canada) change

14:00 - 15:30	FM for Program Analysis and Verification NFM 2024 at Ballroom Chair(s): Douglas Smith Kestrel Institute

14:00 25m Talk		Quantitative Input Usage Static Analysis NFM 2024 Denis Mazzucato INRIA & École Normale Supérieure \| Université PSL, Marco Campion INRIA & École Normale Supérieure \| Université PSL, Caterina Urban Inria & École Normale Supérieure \| Université PSL
14:25 25m Talk		Verifying a C implementation of Derecho's coordination mechanism using VST and Coq NFM 2024 Ramana Nagasamudram Stevens Institute of Technology, Lennart Beringer Princeton University, Ken Birman Cornell University, Mae Milano Princeton University, David Naumann Stevens Institute of Technology
14:50 25m Talk		Verification of Scapegoat Trees using Dafny NFM 2024 Jiapeng Wang East China Normal University, Sini Chen East China Normal University, Huibiao Zhu East China Normal University
15:15 15m Talk		Real Arithmetic in TLAPM NFM 2024 Ovini V.W. Gunasekera Lancaster University, Andrew Sogokon Lancaster University, Antonios Gouglidis Lancaster University, Neeraj Suri