@inbook{23e140cdb78b4fecbd5db8aacfb6f15a,
title = "A Program Logic for C11 Memory Fences",
abstract = "We describe a simple, but powerful, program logic for reasoning about C11 relaxed accesses used in conjunction with release and acquire memory fences. Our logic, called fenced separation logic (FSL), extends relaxed separation logic with special modalities for describing state that has to be protected by memory fences. Like its precursor, FSL allows ownership transfer over synchronizations and can be used to verify the message-passing idiom and other similar programs. The soundness of FSL has been established in Coq.",
author = "Marko Doko and Viktor Vafeiadis",
year = "2016",
doi = "10.1007/978-3-662-49122-5_20",
language = "English",
isbn = "9783662491218",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "413--430",
editor = "Barbara Jobstmann and Leino, {K. Rustan M.}",
booktitle = "Verification, Model Checking, and Abstract Interpretation. VMCAI 2016",
}