Differences

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

--- slin [2013/06/24 11:38]
losa
+++ slin [2013/12/09 10:18] (current)
losa
@@ Line 1: / Line 1: @@
 ====== Speculative Linearizability ======
 ===== Automata Specification in Isabelle/HOL =====
@@ Line 11: / Line 9: @@
 [[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: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}}