Lab for Automated Reasoning and Analysis 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

I/O automata with finite trace semantics in Isabelle/HOL

slin.txt · Last modified: 2013/12/09 10:18 by losa