Interactive Verification on Intermediate Language

ivil 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 phi)
  
• assumptions (assume phi)
  
• anonymisations (havoc x)
  
• assignments (x := t)
• indeterministic branching (goto n₁ n₂)
  

ivil can translate proof obligations to SMTLib input. The result of SMT solvers (such as Z3) can be used to close subgoals in ivil.

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.