Project

General

Profile

Skype Meeting 06092016 » History » Version 11

Sepideh Asadi, 06/09/2016 22:08

1 2 Sepideh Asadi
h1. Skype Meeting 06092016
2 3 Sepideh Asadi
3 4 Sepideh Asadi
*Updates of current tasks:*
4 3 Sepideh Asadi
5 11 Sepideh Asadi
Antti: works on incrementality- added some bugs to Issue-tracking
6 3 Sepideh Asadi
7 9 Sepideh Asadi
Karine: is working on new version of CBMC- and refinement.
8 3 Sepideh Asadi
9 10 Sepideh Asadi
Sepideh: is doing experiments on FF-HF-CBMC
10
sepideh has found some benchmarks that CBMC gets out of memory, but HiFrog and Funfrog managed to do verification very quickly.
11
Benchmarks: EvenOdd.c, Arith.c, in recursion directory
12 1 Sepideh Asadi
13 10 Sepideh Asadi
reports some bugs: rec4.c  in 17_recursion
14 7 Sepideh Asadi
15 8 Sepideh Asadi
=========================================
16
17 3 Sepideh Asadi
*Things we agreed to do this week:*
18 1 Sepideh Asadi
19 9 Sepideh Asadi
20 6 Sepideh Asadi
Antti: Uploaded the benchmark of Milano guys, FABRIZIO PASTORE,(also will upload more)
21 3 Sepideh Asadi
22
23
Karine:
24 1 Sepideh Asadi
25 9 Sepideh Asadi
26 6 Sepideh Asadi
Sepideh:
27 1 Sepideh Asadi
1) We need to know how consistent the results of experiment are, so Sepideh will prepare Scatter plot, and compare the results.
28 6 Sepideh Asadi
2) she will do experiment on Milano guys' benchmark.
29 9 Sepideh Asadi
3) benchmarking the OpenSMT2 incrementality implementation 
30 7 Sepideh Asadi
31
--------------
32
We need to have proper benchmark for interpolation.