PerSeVerE: Persistency Semantics for Verification under Ext4 (POPL 2021 - POPL Research Papers) - POPL 2021

Write a Blog >>

Sun 17 - Fri 22 January 2021 Online

Who

Michalis Kokologiannakis, Ilya Kaysin, Azalea Raad, Viktor Vafeiadis

Track

Time Zone

The program is currently displayed in (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna.

Use conference time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, ViennaSelect 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

Fri 22 Jan 2021 16:35 - 16:45 at POPL-B - Concurrency (Message Passing)

Abstract

Although ubiquitous, modern filesystems have rather complex behaviour that is hardly understood by programmers and leads to severe software bugs, such as data corruption. As a first step to ensure correctness of software performing file I/O, we formalize the semantics of the Linux ext4 filesystem, which we integrate with the weak memory consistency semantics of C/C++. We further develop an effective model checking approach for verifying programs that use the filesystem, and also report bugs in commonly-used text editors.

Link to Publication

https://dl.acm.org/doi/pdf/10.1145/3434324

DOI

https://doi.org/10.1145/3434324

Michalis Kokologiannakis

MPI-SWS, Germany

Greece

Ilya Kaysin

National Research University Higher School of Economics, JetBrains Research

Russia

Azalea Raad

Imperial College London

Viktor Vafeiadis

MPI-SWS

Germany

Time Zone

The program is currently displayed in (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna.

Use conference time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, ViennaSelect 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

Fri 22 Jan
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

	15:45 - 16:45	Concurrency (Message Passing)POPL at POPL-B

	15:45 10m Talk		On Algebraic Abstractions for Concurrent Separation Logics POPL František Farka IMDEA Software Institute, Spain, Aleksandar Nanevski IMDEA Software Institute, Anindya Banerjee IMDEA Software Institute, Germán Andrés Delbianco Nomadic Labs, Ignacio Fábregas Universidad Complutense de Madrid Link to publication DOI
	15:55 10m Talk		Transfinite Step-Indexing for Termination POPL Simon Spies MPI-SWS and University of Cambridge, Neel Krishnaswami Computer Laboratory, University of Cambridge, Derek Dreyer MPI-SWS Link to publication DOI
	16:05 10m Talk		Precise Subtyping for Asynchronous Multiparty Sessions POPL Silvia Ghilezan University of Novi Sad, Mathematical Institute SASA, Jovanka Pantović University of Novi Sad, Ivan Prokić University of Novi Sad, Alceste Scalas Technical University of Denmark, Nobuko Yoshida Imperial College London Link to publication DOI Media Attached
	16:15 10m Talk		A Separation Logic for Effect Handlers POPL Paulo Emílio de Vilhena Inria, François Pottier Inria, France Link to publication DOI
	16:25 10m Talk		Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic POPL Léon Gondelman Aarhus University, Simon Oddershede Gregersen Aarhus University, Abel Nieto Aarhus University, Amin Timany Aarhus University, Lars Birkedal Aarhus University Link to publication DOI
	16:35 10m Talk		PerSeVerE: Persistency Semantics for Verification under Ext4 POPL Michalis Kokologiannakis MPI-SWS, Germany, Ilya Kaysin National Research University Higher School of Economics, JetBrains Research, Azalea Raad Imperial College London, Viktor Vafeiadis MPI-SWS Link to publication DOI