There are the following examples in the psyco project:

istaa2013.security: works fine 17.06.2016

Search:

k = 2

states = 3

Interpolation:

states = 5

input = 6

istaa2013.net: is finite

Search:

k = 8

States = 160

Interpolation:

states = 42

input = 59

Time: 330 seconds for the search, up to 30 minutes.

issta2013.math: works fine, no state but a lot of possible reached errors.

k = 1

states = 0

issta2013.io: runs and terminates quickly.

Search:

k = 2

states = 2

Interpolation:

states = 4

input = 6

issta2013.cev: As long as all transitions with undefined loop are left out, it terminates.

k=5

The following method in combination or standalone lead to a infinite loop:

-reset

-lsamAscentBurn

-lsamAscentRendezvous

-lsamRendevouz

time: overall roughly a minute, 13 seconds the search, and reaches more or less 35 states.

gsoc.cev_esas: The transition system of the new modle is complete.

Search:

k = 7

states = 72

Interpolation:

states = 20

input = 21

time = 34 seconds search, total up to 20 minutes

gsoc.cev_esas with state machine in the cev (CEV_1.java):

Search:

k = 13

states = 31

Interpolation:

states = -

input = -

time = 244 seconds for the search, 255 seconds overall

issta2013.accelerometer: infinite transition system. DataReceived is not limited.

issta2013.abp: infinite loop right know. No constraint on the var expect. Does not terminate!

I want to add a few further thoughts about quantifier elimination:

• Is not reliable faster than normal reasoning with quantifier.

((exists ('pp_2':sint32): ((('uVarReplacement_1' < 5) && ('uVarReplacement_1' == 0)) && ('this.x' == ('uVarReplacement_1' + 'pp_2')))) && !('this.x' == 0)) is not transformed within 5 minutes, but the complete search is done in less than a minute without quantifier elimination.

Reasons for the heavy runtime:

-Many small variables in the assignment which are not bound to a value => a lot of quantifier. Especially the reset method in the cev example is nasty.

-Complex new state description without any change to the original state. The state difference algorithm runs nevertheless quite long.

-Parts in the symbolic state description, that are not needed. In case a literal is assigned, the state history can be cut.

Ideas for optimization:

-Remove already reached error paths => They cannot be reached twice => Done

-Paths conditions, that are always true don't need a check. Further they do not need to be included in the state description. => works fine. Done

-In case of static value assignment, the history can be cut. => Done

-Simplifed state description and state history, so that difference checking speeds up. => Works nice. Done

-Check path result for affect on the result, otherwise do not execute the transition. => Works fine. Done

-Check the transition system previously on a bound for the variable within the transition => infinite loop detection ? Declined