IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness. It also provides a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.
IVy is joint work with the following people:
- Oded Padon, Tel Aviv University
- Aurojit Panda, UC Berkeley
- Mooly Sagiv, Tel Aviv University
- Sharon Shoham, Academic College of Tel Aviv Yaffo
IVy is an open source project hosted by GitHub.
There is an introduction to Ivy including a VM.