Treffer: Formal Methods for Correct Persistent Programming (Dagstuhl Seminar 23412)

Title:
Formal Methods for Correct Persistent Programming (Dagstuhl Seminar 23412)
Authors:
Ori Lahav and Azalea Raad and Joseph Tassarotti and Viktor Vafeiadis and Anton Podkopaev, Lahav, Ori, Raad, Azalea, Tassarotti, Joseph, Vafeiadis, Viktor, Podkopaev, Anton
Publisher Information:
Schloss Dagstuhl – Leibniz-Zentrum für Informatik 2024
Document Type:
E-Ressource Electronic Resource
Index Terms:
concurrency, formal methods, non-volatile-memory, persistency, verification, Article, Text, doc-type:ResearchArticle, publishedVersion
DOI:
10.4230.DagRep.13.10.50
URL:
https://drops.dagstuhl.de/entities/document/10.4230/DagRep.13.10.50
Availability:
Open access content. Open access content
https://creativecommons.org/licenses/by/4.0/legalcode
Note:
application/pdf
English
Other Numbers:
DEDAG oai:drops-oai.dagstuhl.de:19833
doi:10.4230/DagRep.13.10.50
urn:nbn:de:0030-drops-198337
1429550033
Contributing Source:
SCHLOSS DAGSTUHL LEIBNIZ ZENTRUM GMBH
From OAIster®, provided by the OCLC Cooperative.
Accession Number:
edsoai.on1429550033
Database:
OAIster

Weitere Informationen

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.