Instructor: Mooly Sagiv

TA: Oded Padon

Workshop meeting: Thursday 17:00-19:00, Dan David 204

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.



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.

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.