30.5.2016

• Malte presented his current state of work, corresponding post image for enumerativ specification. Falk outlines a problem, if the increment value is not static:

  #!java
  
  public class FirstExample {
    @Symbolic("true")
    private int x = 0;
  
    public void m1(){
      if(x<5){
        x = x + p;
      }else{
        assert false;
      }
    }
  }
  

  Quantifier elimination is necessary to determine, whether New' is still non empty, because the values for p are not further specified.

Quantifier Elimination Example

New region after the first iteration looks like: (unique_0 == 0) && (this.x == unique_0 + p1).

In the second iteration leeds to: (unique_0 == 0) && (unique2 == unique_0 + p1) && (this.x == unique_2 + p2)

So for difference we need to verify (newRegion && !reachableRegion) which leads to:

#!plain


(exists p1, p2: (unique_0 == 0) && (unique2 == unique_0 + p1) && (this.x == unique_2 + p2)) 
&& !(forall p3: ((unique_0 == 0) && (this.x == unique_0 + p1)).

17.06.2016

-Demonstrated first examples of the symbolic search -Discussed a few implementation details

goals for next week:

-> extend symbolic search for the usage of the quantifier elimination

-> evaluate which of the psyco examples can be handled right now with this implementation

-> The current state of the examples is listed here

24.06.2016

The main problem is, that termination is not guaranteed by the search itself. Also some of the current Psyco examples need a lot of time to calculate the next iteration. It does not make sense to speed them up, as long as it is unknown, whether the search is going to finish or not.

Therefore we will experiment with a few static analysis techniques next in upfront to the search on the transition system. The goal is to determine transitions, that change variables without any limit in the path condition. The goal is to find a system invariant for all limited variables and over approximate the visible states using this invariant. Then we check reachability of this states.

The next goal for the second part of the GSOC coding phase is to get a reasoning about termination of the search. In case the search is not going to terminate, we apply a heuristic based on the previous described over approximation to estimate reasonable values for k.

We will focus on this kinds of improvements towards the search result and not on any improvement for the state description solving. So OBDD are not considered in this project and we will stay with the capabilities of Z3.