(Given at Tel Aviv University in Spring 2017-2018)

Distributed algorithms are an appealing target for formal verification: they are very important, and and their correctness can be tricky and subtle. In this workshop, we will verify distributed and concurrent algorithms the using Ivy verification system.

Teams comprise of 2-3 students, and the projects must be complete and approved by the course staff before 14/6/2018. On 14/6/2018 we will meet and each team will present their project.

Workshop forum

During the semester, we will communicate via email and via the workshop forum.

Schedule

• 8/3 Welcome
• 15/3 Introduction to Ivy (client_server example, leader example)
• 22/3 Projects kickoff
  • Before the meeting, each team should select a project / protocol, and start to read about it and model it in Ivy
• ... Independent work in teams, meetings as needed
• 14/6 Project presentations

Ivy

Ivy is a deductive verification system based on decidable fragments of first-order logic. Ivy is open source, and hosted on GitHub.

For your conveneince, we provide a virtual machine that has Ivy installed. To run the virtual machine, use VirtualBox version 5.2.8 or later. The VM should be logged on with the user name ivyuser and password ivy.

Possible Projects

Please use this document to assing teams and projects (TAU mail account required, send me an email if you need other access).

Use Ivy to verify algorithms

Below are some ideas for algorithms to verify. Each category is open ended, and you can suggest any distributed algorithm that you are interested in.

• Shared Memory Mutual Exclusion
  • Dijkstra's 1965 algorithm
  • N. G. de Bruijn's 1967 algorithm
  • Knuth's 1966 algorithm
  • Eisenberg & McGuire algorithm (Wikipedia)
  • Lamport's Bakery algorithm
  • Lamport's 1 bit algorithm (Figure 1, page 17 of The Mutual Exclusion Problem Part II: Statement and Solutions)
  • Algorithms from James H. Anderson's Lamport on Mutual Exclusion: 27 years of Planting seeds
    • Bakery algorithm (Figure 1)
    • Lamport's fast mutual exclusion algorithm (Figure 2)
    • Timestamp algorithm (Figure 4)
  • Szymański's algorithm
  • Peterson's algorithm
  • ...
• Distributed Mutual Exclution
  • Lamport's distributed mutual exclusion algorithm
  • Ricart–Agrawala algorithm
  • Raymond's algorithm
  • Maekawa's algorithm
  • Suzuki–Kasami algorithm
  • ...
• Paxos Variants. See Paxos Made Moderately Complex for a nice overview. Note that some are already verified with Ivy.
  • Disk Paxos
  • Cheap Paxos
  • Generalized Paxos
  • Mencius
  • Egalitarian Paxos
  • ...
• Blockchain algorithms
  • Algorand
  • Honey Badger BFT
  • Bitcoin-NG
  • ...

Improve Ivy

Another option for a project is to add or improve some feaature of Ivy itself. Ivy is written in Python. Below are some ideas.

• Connect Ivy to automated theorem provers other than Z3, and experiment witht their performance
• Improve Ivy's counterexample presentation to make it more user friendly
• ...