Differences

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

--- slin [2012/03/29 10:54]
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}}
-[[http://afp.sourceforge.net/entries/Abortable_Linearizable_Modules.shtml|Abortable Linearizable Modules in the AFP]]
-===== Trace-Based Specification in Isabelle/HOL =====
+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]]
-{{slin:tracespec.txt|Specification}}
+===== 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}}
+{{slin:speclin.tar.gz|TLA+ Specifications}}
-===== Technical Report =====
+===== I/O automata with finite trace semantics in Isabelle/HOL =====
-[[http://infoscience.epfl.ch/record/170038?ln=en|Technical Report at infoscience.epfl.ch]]
-{{slin:main.pdf|Fulltext}}
+{{slin:ioa.tar.gz|IOA framework with finite trace semantics}}