SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Wed 18 Nov 2020 15:20 - 15:40 at SPLASH-I - W-5 Chair(s): Mohsen Lesani, Dan Barowy
Thu 19 Nov 2020 03:20 - 03:40 at SPLASH-I - W-5 Chair(s): Nengkun Yu, Filip Křikava

The advent of non-volatile memory (NVM) technologies is expected to transform how
software systems are structured fundamentally, making the task of \emph{correct} programming significantly harder.
This is because ensuring that memory stores persist in the correct order is challenging,
and requires low-level programming to flush the cache at appropriate points.
This has in turn resulted in a noticeable \emph{verification gap}.
%causing a significant verification burden.

To address this, we study the verification of NVM programs, and present \emph{Persistent
Owicki-Gries} (POG), the first program logic for reasoning about such programs.
We prove the soundness of POG over the recent Intel-x86 model, which formalises
the out-of-order persistence of memory stores and the semantics of the Intel
cache line flush instructions. We then use POG to verify several programs that interact with NVM.

Wed 18 Nov
Times are displayed in time zone: Central Time (US & Canada) change

15:00 - 16:20: W-5OOPSLA at SPLASH-I +12h
Chair(s): Mohsen LesaniUniversity of California at Riverside, USA, Dan BarowyWilliams College
15:00 - 15:20
Talk
OOPSLA
Thodoris SotiropoulosAthens University of Economics and Business, Stefanos ChaliasosAthens University of Economics and Business, Dimitris MitropoulosAthens University of Economics and Business, Diomidis SpinellisAthens University of Economics and Business
Link to publication DOI Pre-print Media Attached
15:20 - 15:40
Talk
OOPSLA
Azalea RaadMPI-SWS / Imperial College London, Ori LahavTel Aviv University, Viktor VafeiadisMPI-SWS
Link to publication DOI Media Attached
15:40 - 16:00
Talk
OOPSLA
Sumit GulwaniMicrosoft, Vu LeMicrosoft, Arjun RadhakrishnaMicrosoft, Ivan RadičekMicrosoft, Mohammad RazaMicrosoft
Link to publication DOI Media Attached
16:00 - 16:20
Talk
OOPSLA
Fangyi ZhouImperial College London, Francisco FerreiraImperial College London, Raymond HuUniversity of Hertfordshire, Rumyana NeykovaBrunel University London, Nobuko YoshidaImperial College London
Link to publication DOI Pre-print Media Attached

Thu 19 Nov
Times are displayed in time zone: Central Time (US & Canada) change

03:00 - 04:20: W-5OOPSLA at SPLASH-I
Chair(s): Nengkun YuUniversity of Technology Sydney, Filip KřikavaCzech Technical University
03:00 - 03:20
Talk
OOPSLA
Thodoris SotiropoulosAthens University of Economics and Business, Stefanos ChaliasosAthens University of Economics and Business, Dimitris MitropoulosAthens University of Economics and Business, Diomidis SpinellisAthens University of Economics and Business
Link to publication DOI Pre-print Media Attached
03:20 - 03:40
Talk
OOPSLA
Azalea RaadMPI-SWS / Imperial College London, Ori LahavTel Aviv University, Viktor VafeiadisMPI-SWS
Link to publication DOI Media Attached
03:40 - 04:00
Talk
OOPSLA
Sumit GulwaniMicrosoft, Vu LeMicrosoft, Arjun RadhakrishnaMicrosoft, Ivan RadičekMicrosoft, Mohammad RazaMicrosoft
Link to publication DOI Media Attached
04:00 - 04:20
Talk
OOPSLA
Fangyi ZhouImperial College London, Francisco FerreiraImperial College London, Raymond HuUniversity of Hertfordshire, Rumyana NeykovaBrunel University London, Nobuko YoshidaImperial College London
Link to publication DOI Pre-print Media Attached