Skype Meeting 06092016¶

Updates of current tasks:

Antti:

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

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

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.