Interactive Verification on Intermediate Language

ivil is a tool for the interactive (better semi-automatic) verification on the level of an intermediate verification language.

At present, this is a proof-of-concept implementation which we plan to extend in the future.

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 used to launch ivil:


Alternatively, you can download either the binary distribution or the source code distribution of ivil.

There is no manual for ivil, yet. The following first and very small examples may help you to understand the general ideas. Please choose "File → Load Problem from URL" from the menu and enter the according URL into the input box.

1. Selection Sort (http://i12www.ira.uka.de/~mulbrich/ivil/selectionSort.p)
   

   *
   * Selection Sort in Pseudo code
   *
   
   given: 
     a ... array of integer
     n ... length of a
     i,j ... index variables
     t ... index variable
   
   selectionSort:
     for each i from 1 to n-1
     invariant: subarray(a, 1..i) is sorted
                a is a permutation of original a
   
        t := i
   
        for each j from i+1 to n
        invariant: for k=i+1..j : a[t] <= a[k]
                   a is a permutation of original a
   
           if a[j] < a[t] then
              t := j
   
        swap t and i in a
   
   post conditions:
     for all applicable i: a[i] <= a[i+1]
     a is a permutation of original a
       

This is a small example in pseudo code example manually translated into the intermediate representation. If you have the SMT solver Z3 installed (i.e., z3 is your path), the example is proccessed automatically.
 
2. Zune Player Bug (http://i12www.ira.uka.de/~mulbrich/ivil/Zune.normaliseDate.p)
   

    
   ...
   while (days > 365) {
       Spec.inline("skip_loopinv " +
           "(* invariant *) sel(h, _this, field_Zune_days) >= 0," +
           "(* variant *) sel(h, _this, field_Zune_days)");
   			
       if (isLeapYear(year)) {
           if (days > 366) {
               days -= 366;
               year += 1;
           }
       } else {
           days -= 365;
           year += 1;
       }
   }
   ...		
       

   This small example is written in the Java programming language. It captures the main problem of the Zune Player Bug.
   Using the SMT solver Z3 all branches of the verification close automatically but one. A counter example can be constructed from the information on the failing branch.
   The intermediate code is generated automatically by a rudimentary Java to intermediate compiler.
    
3. Fixed Zune Player Code (http://i12www.ira.uka.de/~mulbrich/ivil/GoodZune.normaliseDate.p)
   If in the above code the bug is repaired, the resulting piece of code can be verified (termination and a simple post condition) automatically using Z3.