Skip to content

Commit

Permalink
[Civl] Fix ChangRoberts (#858)
Browse files Browse the repository at this point in the history 
This PR provides a new proof for the Chang Roberts protocol for leader
election. The new proof is different from the existing Civl proof in two
ways:
- Stronger specification is proved. The new proof proves that a unique
leader will be elected in all terminal states. The old proof only proved
that conflicting leaders are not elected.
- The modeling of the protocol avoids the use of channels and achieves
all communication asynchronous calls.

---------

Co-authored-by: Shaz Qadeer <[email protected]>
  • Loading branch information
@shazqadeer
shazqadeer and Shaz Qadeer authored Mar 9, 2024
1 parent cf5609f commit 6e9cce4
Show file tree
Hide file tree
Showing 2 changed files with 109 additions and 214 deletions.
Loading

0 comments on commit 6e9cce4

Please sign in to comment.