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.
Перейти к файлу
Ken McMillan 9f3c7ecc0b install.md change 2020-09-04 11:38:51 -07:00
.vscode update `.vscode/settings.json` with more ignore patterns. 2017-05-11 15:26:53 -07:00
bin fixing ivy_test 2016-06-04 10:12:59 -07:00
doc install.md change 2020-09-04 11:38:51 -07:00
examples update chord2s example 2020-02-26 15:58:35 -08:00
ivy fix regressions in arith_proofs branch 2020-08-26 11:34:15 -07:00
lib/emacs working on proof documentation 2020-07-27 14:16:52 -07:00
notebooks adding examples, notebooks 2015-12-28 13:09:12 -08:00
scripts/setup Add missing pydot dependency 2019-12-02 12:06:15 -08:00
submodules z3 submodule update 2019-09-13 12:19:39 -07:00
test fix regressions in arith_proofs branch 2020-08-26 11:34:15 -07:00
vs/ext from class dry run 2017-05-03 13:10:09 -07:00
.gitattributes update `.gitattributes` for shell scripts. 2017-02-22 15:16:58 -08:00
.gitignore more forgotten files 2018-11-23 11:55:23 -08:00
.gitmodules adding picotls as submodule 2019-09-12 17:39:59 -07:00
INSTALL adding examples, notebooks 2015-12-28 13:09:12 -08:00
PACKAGING.md preparing for 1.7.0 2020-02-19 16:32:22 -08:00
README.md README.md change 2020-09-04 11:34:14 -07:00
Vagrantfile vagrant: got ivy gui working over ssh with x11 forwarding. 2017-05-11 13:05:14 -07:00
build_submodules.py separate v2 comiler build 2020-02-19 15:35:39 -08:00
build_v2_compiler.py separate v2 comiler build 2020-02-19 15:35:39 -08:00
license.txt adding license.txt 2015-12-27 21:16:33 -08:00
setup.py forgot pydot 2020-02-19 16:34:47 -08:00

README.md

ivy

Starting Sep. 5, 2020, Ivy development is moving to https://github.com/kenmcmil/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.

Installation

Linux

On Debian-based Linux ditributions such as Ubuntu, download and install the file ms-ivy_X.X_YYYY.deb where X.X is the IVy version and YYYY is the machine architecture. Use your systems package manager to install this package, or the following commands:

$ sudo dpkg -i ms-ivy_X.X_YYYY.deb
$ sudo apt-get install -f

The first command will report missing dependencies, which will be installed by the second command.

Windows

The Windows binary distribution is in the form of a zip archive. Download the file ivy.X.Y-.Windows-z86.zip, where X.X is the IVy version (this will work on both 32-bit and 64 bit Intel Windows). Use Windows Explorer to extract this archive in the directory C:\. This should give you a directory C:\ivy. To use IVy in a command window, first execute this command:

> C:\ivy\scripts\activate

Further Reading

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