[go: up one dir, main page]
More Web Proxy on the site http://driver.im/

Formal Methods for Correct Persistent Programming (Dagstuhl Seminar 23412)

Authors Ori Lahav, Azalea Raad, Joseph Tassarotti, Viktor Vafeiadis, Anton Podkopaev and all authors of the abstracts in this report



PDF
Thumbnail PDF

File

DagRep.13.10.50.pdf
  • Filesize: 2.26 MB
  • 15 pages

Document Identifiers

Author Details

Ori Lahav
  • Tel Aviv University, IL
Azalea Raad
  • Imperial College London, GB
Joseph Tassarotti
  • New York University, US
Viktor Vafeiadis
  • MPI-SWS - Kaiserslautern, DE
Anton Podkopaev
  • JetBrains - Amsterdam, NL
and all authors of the abstracts in this report

Cite As Get BibTex

Ori Lahav, Azalea Raad, Joseph Tassarotti, Viktor Vafeiadis, and Anton Podkopaev. Formal Methods for Correct Persistent Programming (Dagstuhl Seminar 23412). In Dagstuhl Reports, Volume 13, Issue 10, pp. 50-64, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/DagRep.13.10.50

Abstract

Recently developed non-volatile memory (NVM) devices provide persistency guarantees along with byte-addressable accesses and performance characteristics that are much closer to volatile random-access memory (RAM). However, writing programs that correctly use these devices is challenging, and bugs related to their use can cause permanent data loss in applications.
This Dagstuhl Seminar brought together experts in a range of areas related to concurrency and persistent memory to explore and develop formal methods for ensuring the correctness of applications that use persistent memory. Talks and discussions at the seminar highlighted challenges related to correctness criteria for concurrent objects using persistent memory, liveness properties of persistent objects, and how changes in NVM and related technologies should shape the development of formal methods for NVM.

Subject Classification

ACM Subject Classification
  • Hardware → Non-volatile memory
  • Theory of computation → Program semantics
  • Theory of computation → Program verification
Keywords
  • concurrency
  • formal methods
  • non-volatile-memory
  • persistency
  • verification

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail