Skype Meeting 06092016¶

Updates of current tasks:

Antti: works on incrementality- added some bugs to Issue-tracking

Karine: is working on new version of CBMC- and refinement.

Sepideh: is doing experiments on FF-HF-CBMC
sepideh has found some benchmarks that CBMC gets out of memory, but HiFrog and Funfrog managed to do verification very quickly.
Benchmarks: EvenOdd.c, Arith.c, in recursion directory

reports some bugs: rec4.c in 17_recursion which HIfrog failed with this error:; Error: Clause has no color (triggered at PGInterAux.C, 218)

=========================================

Things we agreed to do this week:

Antti: Uploaded the benchmark of Milano guys, FABRIZIO PASTORE,(also will upload more)

Karine:

Sepideh:
1) We need to know how consistent the results of experiment are, so Sepideh will prepare Scatter plot, and compare the results.
2) she will do experiment on Milano guys' benchmark.
3) benchmarking the OpenSMT2 incrementality implementation

--------------
We need to have proper benchmark for interpolation.