LoreonLabsPlatform

Overview

Intelligence

Markets
Builders
Research
Ecosystems
Launchpads

Search

Dafny

lets-prove-blocking-queue

Proving a blocking queue deadlock free in a dozen different ways

DafnyEmergingalgorithmconcurrencydeadlock-freedomproof

Stars

45

Forks

5

Contributors

3

Last push

2mo ago

Recent commits

Latest commits.

Strengthen TypeOK condition to include buffer type validation to make TLAPS 1.6 accept the proof.
f5c7db2Markus Alexander Kuppe2mo ago
Update GitHub Actions workflow to install TLAPS from the latest release and adjust run commands accordingly.
e195eddMarkus Alexander Kuppe2mo ago
Update GitHub Actions workflow to use actions/checkout@v4.
aa85d5aMarkus Alexander Kuppe2mo ago
SPARK submission (#3)
c1a800cJohannes Kanig20mo ago
Add link to https://github.com/dricketts/teaching-concurrency
81ba935

Markus Alexander Kuppe

61mo ago

Set up Dafny extension on Gitpod.

300fb11Markus Alexander Kuppe75mo ago

Install newest TLA+ extension.

2162dd1Markus Alexander Kuppe75mo ago

Setup for gitpod (online VSCode-alike IDE).

af457f5Markus Alexander Kuppe75mo ago

Top contributors

Builders behind this project.