Differences

This shows you the differences between two versions of the page.

--- slin [2012/03/05 11:47]
losa
+++ slin [2013/12/09 10:18]
losa
@@ Line 1: / Line 1: @@
 ====== Speculative Linearizability ======
 ===== 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]]
-===== Trace-Based Specification in Isabelle/HOL =====
+===== TLA+ Specifications =====
-{{slin:tracespec.txt|Specification}}
+{{slin:speclin.tar.gz|TLA+ Specifications}}
-{{slin:lcp.txt|Definition and proofs about the longest common prefix of a set of lists}}
-{{slin:listfuns.txt|Recursive functions on lists}}
-{{slin:ioa.zip|IOA framework with finite trace semantics}}
+===== I/O automata with finite trace semantics in Isabelle/HOL =====
-===== Technical Report =====
-[[http://infoscience.epfl.ch/record/170038?ln=en|Technical Report]]
+{{slin:ioa.tar.gz|IOA framework with finite trace semantics}}
-{{slin:main.pdf|Fulltext}}