Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Iris
examples
Commits
06827859
Commit
06827859
authored
Jun 30, 2020
by
Ralf Jung
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
README: make link texts consistent with folder names
parent
77ea6399
Pipeline
#30792
passed with stage
in 25 minutes and 51 seconds
Changes
1
Pipelines
9
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
4 additions
and
4 deletions
+4
-4
README.md
README.md
+4
-4
No files found.
README.md
View file @
06827859
...
...
@@ -61,17 +61,17 @@ This repository contains the following case studies:
-
Treiber Stack (by Zhen Zhang, and another version by Rodolphe Lepigre).
-
Flat Combiner (by Zhen Zhang, also see
[
this archived documentation
](
https://gitlab.mpi-sws.org/FP/iris-atomic/tree/master/docs
)
).
*
[
spanning
-
tree
](
theories/spanning_tree
)
: Proof of a concurrent spanning tree
*
[
spanning
_
tree
](
theories/spanning_tree
)
: Proof of a concurrent spanning tree
algorithm (by Amin Timany).
*
[
concurrent
-
stacks
](
theories/concurrent_stacks
)
: Proof of an implementation of
*
[
concurrent
_
stacks
](
theories/concurrent_stacks
)
: Proof of an implementation of
concurrent stacks with helping by Daniel Gratzer et. al., as described in the
[
report
](
http://iris-project.org/pdfs/2017-case-study-concurrent-stacks-with-helping.pdf
)
.
*
[
lecture
-
notes
](
theories/lecture_notes
)
: Coq examples for the
*
[
lecture
_
notes
](
theories/lecture_notes
)
: Coq examples for the
[
Iris lecture notes
](
http://iris-project.org/tutorial-material.html
)
.
*
[
hocap
](
theories/hocap
)
: Formalizations of the concurrent bag and concurrent
runners libraries from the
[
HOCAP paper
](
https://dl.acm.org/citation.cfm?id=2450283
)
(by Dan Frumin). See the associated
[
README
](
theories/hocap/README.md
)
.
*
[
array
-
based_queuing_lock
](
/theories/array_based_queuing_lock
)
: Proof of
*
[
array
_
based_queuing_lock
](
/theories/array_based_queuing_lock
)
: Proof of
safety of an implementation of the array-based queuing lock. This example is
also covered in the chapter
[
"Case study: The Array-Based Queueing
Lock"
](
https://iris-project.org/tutorial-pdfs/iris-lecture-notes.pdf#section.10
)
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment