IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide 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.
Перейти к файлу
Michael Lowell Roberts b53fa51b7c simplify `Vagrantfile`. 2017-02-28 07:40:13 -08:00
.vscode exclude files in vscode workspace settings. 2017-02-21 16:31:25 -08:00
bin fixing ivy_test 2016-06-04 10:12:59 -07:00
doc fixed problems with implicit imports 2016-10-24 18:10:29 -07:00
examples fixed problems with implicit imports 2016-10-24 18:10:29 -07:00
ivy removed some debug prints 2016-10-24 18:15:38 -07:00
lib/emacs adding mixord and "delegate to" 2016-04-26 18:34:58 -07:00
notebooks adding examples, notebooks 2015-12-28 13:09:12 -08:00
scripts/setup z3 now works in vagrant environment. 2017-02-19 14:33:37 -08:00
submodules added vagrantfile, z3 submodule, and setup scripts. 2017-02-16 08:34:42 -08:00
test fixed run_expects 2016-10-19 12:18:31 -07:00
.gitattributes update `.gitattributes` for shell scripts. 2017-02-22 15:16:58 -08:00
.gitignore added vagrantfile, z3 submodule, and setup scripts. 2017-02-16 08:34:42 -08:00
.gitmodules added vagrantfile, z3 submodule, and setup scripts. 2017-02-16 08:34:42 -08:00
INSTALL adding examples, notebooks 2015-12-28 13:09:12 -08:00
README.md fixing README 2016-05-26 17:26:32 -07:00
Vagrantfile simplify `Vagrantfile`. 2017-02-28 07:40:13 -08:00
license.txt adding license.txt 2015-12-27 21:16:33 -08:00
setup.py working on networking doc 2016-08-16 18:59:35 -07:00

README.md

ivy

IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide 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.

For further information on IVy, see the IVy web site.