Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
slin [2012/03/05 11:47] 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]] | ||
Line 17: | Line 21: | ||
===== Technical Report ===== | ===== Technical Report ===== | ||
- | [[http://infoscience.epfl.ch/record/170038?ln=en|Technical Report]] | + | [[http://infoscience.epfl.ch/record/170038?ln=en|Technical Report at infoscience.epfl.ch]] |
{{slin:main.pdf|Fulltext}} | {{slin:main.pdf|Fulltext}} | ||