Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Last revision Both sides next revision | ||
slin [2012/03/29 10:54] losa |
slin [2013/06/24 11:38] losa |
||
---|---|---|---|
Line 1: | Line 1: | ||
====== Speculative Linearizability ====== | ====== Speculative Linearizability ====== | ||
+ | |||
===== Automata Specification in Isabelle/HOL ===== | ===== Automata Specification in Isabelle/HOL ===== | ||
- | Our automata specification can be found in the Archive of Formal Proof at the following URL: | + | {{slin:alm.tar.gz|Archive containing the theory files}} |
+ | |||
+ | An older version of the theory can be found in the Archive of Formal Proofs. | ||
[[http://afp.sourceforge.net/entries/Abortable_Linearizable_Modules.shtml|Abortable Linearizable Modules in the AFP]] | [[http://afp.sourceforge.net/entries/Abortable_Linearizable_Modules.shtml|Abortable Linearizable Modules in the AFP]] | ||