Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

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