Summary

Non-volatile memory (NVM) is an emerging technology that provides orders of magnitude faster access to persistent storage (which preserves its contents after a crash or a power failure) than hard disks.

While NVM is expected to radically change how we manage storage in applications, its programming model is standing on very shaky foundations. The persistency semantics of the mainstream architectures is unclear and full of counterintuitive behaviours. As a result, writing correct NVM programs is extremely difficult.

The project's goal is to develop a solid mathematical basis for determining the possible outcomes of persistent programs and reasoning about their correctness. More specifically, we aim to produce:

Project publications

Other relevant publications


This project is funded from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No. 101003349).

Imprint | Data protection