Embedding Hindsight Reasoning in Separation Logic

Roland Meyer, Thomas Wies, Sebastian Wolff

Research output: Contribution to journalArticlepeer-review


Automatically proving linearizability of concurrent data structures remains a key challenge for verification. We present temporal interpolation as a new proof principle to guide automated proof search using hindsight arguments within concurrent separation logic. Temporal interpolation offers an easy-to-automate alternative to prophecy variables and has the advantage of structuring proofs into easy-to-discharge hypotheses. Additionally, we advance hindsight theory by integrating it into a program logic, bringing formal rigor and complementary proof machinery. We substantiate the usefulness of temporal interpolation by implementing it in a tool and using it to automatically verify the Logical Ordering tree. The proof is challenging due to future-dependent linearization points and complex structure overlays. It is the first formal proof of this data structure. Interestingly, our formalization revealed an unknown bug and an existing informal proof as erroneous.

Original languageEnglish (US)
Article number182
JournalProceedings of the ACM on Programming Languages
StatePublished - Jun 6 2023


  • Hindsight
  • Linearizability
  • Logical Ordering Tree

ASJC Scopus subject areas

  • Software
  • Safety, Risk, Reliability and Quality


Dive into the research topics of 'Embedding Hindsight Reasoning in Separation Logic'. Together they form a unique fingerprint.

Cite this