Interactive Verification on Intermediate Languageivil is a tool for the interactive (better semi-automatic) verification on the level of an intermediate verification language.
This is a proof-of-concept implementation. Current Version: 0.20
The verification language which is used in ivil is embedded into a special dynamic logic. It is closely related - yet not entirely identical - to BoogiePL and is unstructured, indeterministic, and side-effect-free. Its basic statements are:
- assertions (assert
- assumptions (assume
- anonymisations (havoc
- assignments (x := t)
- indeterministic branching (goto
The Java Webstart Technology can be used to launch ivil:
Alternatively, you can download either the binary distribution or the source code distribution of ivil.
Be sure that you have the SMT solver Z3 installed on which the tool relies. You can download Z3 here.
When starting ivil, you can launch a number of smaller examples by choosing "File → Samples". The examples are explained within the tool.