Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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}}
  
  
  
 
slin.txt · Last modified: 2013/12/09 10:18 by losa