Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
slin [2013/06/24 11:38] losa |
slin [2013/12/09 10:18] (current) losa |
||
---|---|---|---|
Line 1: | Line 1: | ||
====== Speculative Linearizability ====== | ====== Speculative Linearizability ====== | ||
- | |||
- | |||
===== Automata Specification in Isabelle/HOL ===== | ===== Automata Specification in Isabelle/HOL ===== | ||
Line 11: | Line 9: | ||
[[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]] | ||
- | ===== 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}} |