Ivy was introduced in a 2016 PLDI paper “Ivy: Safety Verification by Interactive Generalization“. Ivy helps proof engineers find inductive invariants for proving code safety properties. One of the authors published helpful slides.
The code is open sourced under the GPL, with an archived version on Microsoft’s Github, which now directs interested parties to kenmcmil/ivy.
Multiple follow-on projects rely on the original Ivy code, as its specification language, RML, guarantees that checking satisfiability for every loop-free program fragment is decidable, facilitating automatic verification. Among such projects are I4, IC3PO, SWISS, and DistAI for automatic proof generation. It is therefore desirable to be able to obtain a functional version of Ivy.
Unfortunately, as of Nov’23, instructions for installing Ivy on the kenmcmil/ivy repo appear outdated, and after spending around an hour, I thought it might be possible to find instructions from other users.
A survey of the 11 most recently updated forks of kenmcmil/ivy (the oldest appears to have been forked around Dec’21), shows several with updates not on the upstream: chinenyeokafor:ivy, formal-verification-research:ivy, fhackett:ivy, verse-lab:ivy, and landonjefftaylor:ivy.
The formal-verification-research README.md appears to have updated instructions for Ubuntu 20.04, with some notes on how to address failures to install pygraphviz, ply, and for pip2 trouble. Have not tried those instructions.
The landonjefftaylor repo adds Homebrew instructions which appear to require some changes to build_submodules.py and changes to setup.py.
fhackett appears to have ported Ivy to python3, but it is unclear how much of the functionality maintains original functionality after the changes; the commit message just says “Port to Python 3 and hack till Raft spec builds+runs“.
chinenyeokafor appears to only modify paths for openssl for Darwin, verse-lab adds some Ivy functionality without updating build scripts or docs.
Following instructions in the formal-verification-research repo on the ic3po ivy clone, and some iteration (adding curl, git, etc.) resulted in this working Dockerfile:
FROM ubuntu:22.04
ARG DEBIAN_FRONTEND=noninteractive
# Install any necessary dependencies
RUN apt-get update && apt-get install -y \
# libraries for Yices 2 \
libgmp-dev gperf autoconf \
# libraries for ivy \
g++ cmake python2 g++ cmake graphviz libgraphviz-dev python2-dev libcgraph6 python-tk tix pkg-config libssl-dev libreadline-dev curl git \
&& rm -rf /var/lib/apt/lists/*
RUN curl -sSL https://bootstrap.pypa.io/pip/2.7/get-pip.py -o get-pip.py
RUN python2 get-pip.py
RUN ln /usr/local/bin/pip2 /usr/bin/pip2
RUN pip2 --version
RUN ln /usr/local/bin/pip /usr/bin/pip
RUN pip --version
RUN pip2 install ply pydot pydot-ng pyparsing==2.1.4 pexpect pygraphviz
# create a link to python2
RUN ln /usr/bin/python2 /usr/bin/python
# Copy the build script into the container
COPY . /root
WORKDIR /root/ic3po/ivy
# build submodules
RUN python2 ./build_submodules.py
# install
RUN python2 setup.py install
Hope this was helpful!