Tree Clocks

Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic

Array-based encodings of tree structures are often preferable to linked or abstract data type-based representations for efficiency …

Qiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur, Ilya Sergey