nekton: A Linearizability Proof Checker

Roland Meyer, Anton Opaterny, Thomas Wies, Sebastian Wolff

Research output: Chapter in Book/Report/Conference proceedingConference contribution


nekton is a new tool for checking linearizability proofs of highly complex concurrent search structures. The tool’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.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 35th International Conference, CAV 2023, Proceedings
EditorsConstantin Enea, Akash Lal
PublisherSpringer Science and Business Media Deutschland GmbH
Number of pages14
ISBN (Print)9783031377051
StatePublished - 2023
Event35th International Conference on Computer Aided Verification, CAV 2023 - Paris, France
Duration: Jul 17 2023Jul 22 2023

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume13964 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference35th International Conference on Computer Aided Verification, CAV 2023


  • flow framework
  • linearizability
  • proof checker
  • separation logic

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'nekton: A Linearizability Proof Checker'. Together they form a unique fingerprint.

Cite this