\begin{abstract}

We define the SLin I/O-automaton and prove its composition property. The SLin
I/O-automaton is at the heart of the Speculative Linearizability framework.
This framework simplifies devising robust distributed algorithms by enabling
their decomposition into independent modules that can be analyzed and proved
correct in isolation. It is particularly useful when working in a distributed
environment, where the need to tolerate faults and asynchrony has made current
monolithic protocols so intricate that it is no longer tractable to check their
correctness. Our theory contains a formalization of simulation proof techniques
in the I/O-automata of Lynch and Tuttle and a typical example of a refinement
proof.

\end{abstract}

{"subset_name": "curated", "file": "formal/afp/Abortable_Linearizable_Modules/document/abstract.tex"}