The following tables summarizes the result of our verification technique on several test files. Each row correspond to one test file and has the following format:

Specification file link | Verified property | ✘ | P/C | Time | Trace |

The result of the experiment is given by the *P/C* column,
where we note *P* when the property is successuly proved,
or *C* when a counter example is found (the property is successuly disproved).
The complete output of the verification program is given by the *trace* file (a description of a typical trace can be found here).
It includes the final abstraction used to prove/disprove the property as a tree automaton,
and a list of all the different ways to type the input pattern.
For some experiments we judged necessary to disable the *constants subtyping phase*
to obtain better performances.
This is indicated by the presence of a *✘* symbol.

A detailed description of the specification file format is given here. Experiments were performed on an Intel® i7-7600U CPU, 4 2.80GHz cores with a timeout time of 120s.

Timbuk specifications | |||||
---|---|---|---|---|---|

insertionSort | sorted(insertionSort A_and_B_list) | P | 0.627 | trace | |

orderedTreeTraversal | sorted (infix-traversal ordered_A_and_B_tree) | P | 4.72 | trace | |

deleteImplies | (member Y AnyList) ∧ (not (eq X Y)) → member Y (delete X AnyList) | P | 0.7 | trace | |

reverseImplies | (sorted L) → (invsorted (reverse L)) | P | 1.402 | trace | |

replaceTree | not (member A (replace A C A_and_B_tree)) | P | 0.751 | trace | |

reverse | invsorted (reverse [A,…A,B,…,B]) | P | 2.352 | trace | |

insertTree | ordered (insert A_and_B_list emptyTree) | - | Timeout | ||

split | let (l1,l2) = split [A,B,A,B,…] in not(member B l1) ∧ (member A l2) | P | 0.688 | trace | |

orderedTree | (ordered ordered_A_and_B_tree) | ✘ | P | 7.097 | trace |

delete | member X (delete X AnyList) is false | P | 0.369 | trace | |

deleteBUG | (member X (deleteBUG X AnyList)) is false | C | 0.32 | trace | |

reverseBUGimplies | (member X L) → (member X (reverseBUG L)) | C | 0.417 | trace | |

orderedTreeTraversalBug | sorted (prefix-traversal ordered_A_and_B_tree) | C | 47.847 | trace |

MoCHi specifications | |||||
---|---|---|---|---|---|

makelist | let L= makelist(X,Y) in null(L) ∨ member(Y,L) | P | 0.49 | trace | |

headReverse | X>0 → hd(reverse(makelist X)) > 0 | P | 1.258 | trace | |

zipUnzip | let l1,l2 = unzip (makelist_of_pairs N) in zip l1 l2 does not throw an exception | - | Timeout | ||

treeDepth | (depth(X)≥0 ∧ depth(Y)≥0) → depth(Node(_,X,Y))>0 | P | 0.919 | trace |

Own specifications | |||||
---|---|---|---|---|---|

incTree | !member(0, inc(T)) | P | 0.423 | trace | |

if | Typing if-the-else | C | 0.023 | trace | |

sorted | all possible regular typings for (sorted L) | C | 0.229 | trace | |

appendTheorem | eql((append L1 L2),nil) ↔ (eql(L1,nil) ∧ eql(L2,nil)) | P | 0.321 | trace | |

iteEvenOdd | if even(X) then odd(s(X)) else odd(X) | P | 0.181 | trace | |

even | all possible regular typings for (even X) | P | 0.111 | trace | |

reverseReverseImplies | (sorted L) → (sorted (reverse (reverse L))) | P | 2.312 | trace | |

evenOdd | Y > 0 => (even(X) ≤> even(power(X,Y))) | P | 0.399 | trace | |

insertionSort2 | member(X,L) ↔ member(X,(insertionSort L)) | P | 0.818 | trace | |

mergeSort | sorted(mergeSort A_and_B_list) | ✘ | P | 1.525 | trace |

mult | (mult X 0) = 0 | P | 0.134 | trace | |

deleteTyping | all possible regular typings for (deleteBug X L) | P | 0.215 | trace | |

equalNat | X = Y => X = X | - | Timeout | ||

mergeSort2 | member(X,L) ↔ member(X,(mergeSortBug L)) | ✘ | - | Timeout | |

plusEven | even(plus(X,X)) | P | 0.167 | trace | |

memberTree | (member X T) ↔ (member X (mirror T)) | P | 4.25 | trace | |

heightTree | ((height T)=2) ↔ (height (mirror T) =2) | - | Timeout | ||

equal | - | Timeout | |||

all-a | allA([cons(A, *|nil)]) = true | P | 0.058 | trace | |

memberAppend | (member X (append L1 L2)) ↔ ((member X L1) ∨ (member X L2)) | P | 0.506 | trace | |

square | (square X) != 2 | P | 0.553 | trace | |

orderedTreePredicate | all possible regular typings for (ordered T) | P | 44.348 | trace | |

equalLength | length (minAndMax nat_list) = 2 | P | 1.626 | trace | |

plusEvenError | even(plus(X,Y)) | C | 0.169 | trace | |

orderedTreePredicate2 | (ordered T)::true | C | 40.792 | trace | |

memberAppendError | (member X (append L1 L2)) ↔ ((member X L1) ∧ (member X L2)) | C | 0.504 | trace | |

insertionSort2BUG | member(X, L) <-> member(X, insertionSort(L)) is false | C | 0.816 | trace | |

simple | Non-deterministic f(X) != false | C | 0.049 | trace | |

appendTheoremBug | eql((appendB L1 L2),nil) ↔ (eql(L1,nil) ∧ eql(L2,nil)) | C | 0.354 | trace |

Timbuk specifications | |||||
---|---|---|---|---|---|

foldRightMult | (foldRight mult nonzero_nat_list 1) is not 0 | - | issue #1 | ||

mapSquare | (filter (eq 2) (map square nat_list)) is empty | - | Timeout | ||

insertionSortHO | (sorted leq (insertionSort leq A_and_B_list)) | - | issue #2 | trace | |

foldLeftPlus | even (foldLeft plus 0 even_nat_list) | - | issue #2 | trace | |

mapPlus | no 0 in (map (plus 1) nat_list) | P | 0.416 | trace | |

filterNz | (forAll nz (filter nz nat_list)) | P | 0.423 | trace | |

mapTree | not (member 0 (map (plus 1) nat_tree) | P | 0.561 | trace | |

filterEven | forall even (filter even nat_list) | P | 0.462 | trace | |

filterEvenBug | exists odd (filter even nat_list) | C | 0.542 | trace | |

insertionSortHObug | sorted (≥) (sort (≤) A_and_B_list) | - | issue #3 | trace |

MoCHi specifications | |||||
---|---|---|---|---|---|

mapFilter | map head (filter nonEmpty nat_list) does not throw an exception | P | 0.906 | trace | |

foldDiv | foldLeft div X (makelist Y) does not throw an exception | P | 0.244 | trace | |

forallLeq | forall (leq 1) (makelist X) | P | 0.4 | trace |

Own specifications | |||||
---|---|---|---|---|---|

exists | all possible regular typings for (exists (eq X) A_and_B_list) | P | 0.275 | trace | |

exprSimplif | - | Timeout | |||

forallNotEquivalentNotExists | (forall (neq A) L) ↔ (not(exists (eq A) L)) | P | 0.541 | trace | |

forallImpliesExists | (not(null(L)) ∧ (forall (eq A) L)) → (exists (eq A) L) | P | 0.53 | trace | |

exists2 | all possible regular typings for (exists P A_and_B_list) | P | 0.413 | trace | |

forall | all possible regular typings for (forall (eq X) A_and_B_list) | P | 0.239 | trace | |

map2AddImplies | !member(0, L1) ∧ !member(0, L2) → !member(0, map2 add L1 L2) | - | Timeout | ||

leq | - | Timeout | |||

mergeSortHO | sorted leq (mergeSort leq A_and_B_list) | ✘ | P | 1.67 | trace |

filterEquivExists | (exists (eq A) L) ↔ (not(null(filter (eq A) L)) | P | 0.816 | trace | |

mergeSortHObug | (sorted geq (mergeSort leq A_and_B_list)) | - | Timeout | ||

forallNotEquivalentNotForall | (forall (neq A) L) ↔ (not(forall (eq A) L)) | C | 0.509 | trace | |

forallImpliesExistsError | (forall (eq A) L) → (exists (eq A) L) | C | 0.462 | trace |