This is an old revision of the document!
Speculative Linearizability
Automata Specification in Isabelle/HOL
Our automata specification can be found in the Archive of Formal Proof at the following URL: Abortable Linearizable Modules in the AFP
Trace-Based Specification in Isabelle/HOL
Specification Definition and proofs about the longest common prefix of a set of lists Recursive functions on lists IOA framework with finite trace semantics