@inproceedings{86ec41c7988c4c1da05509cb9d6f3b8a,
title = "nekton: A Linearizability Proof Checker",
abstract = "nekton is a new tool for checking linearizability proofs of highly complex concurrent search structures. The tool{\textquoteright}s unique features are its parametric heap abstraction based on separation logic and the flow framework, and its support for hindsight arguments about future-dependent linearization points. We describe the tool, present a case study, and discuss implementation details.",
keywords = "flow framework, linearizability, proof checker, separation logic",
author = "Roland Meyer and Anton Opaterny and Thomas Wies and Sebastian Wolff",
note = "Publisher Copyright: {\textcopyright} 2023, The Author(s).; 35th International Conference on Computer Aided Verification, CAV 2023 ; Conference date: 17-07-2023 Through 22-07-2023",
year = "2023",
doi = "10.1007/978-3-031-37706-8_9",
language = "English (US)",
isbn = "9783031377051",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "170--183",
editor = "Constantin Enea and Akash Lal",
booktitle = "Computer Aided Verification - 35th International Conference, CAV 2023, Proceedings",
address = "Germany",
}