LARA Speculative Linearizability Automata Specification in Isabelle/HOL Archive containing the theory files An older version of the theory can be found in the Archive of Formal Proofs. Abortable Linearizable Modules in the AFP TLA+ Specifications TLA+ Specifications I/O automata with finite trace semantics in Isabelle/HOL IOA framework with finite trace semantics
