Skype Meeting 06092016 » History » Version 16
Karine Even Mendoza, 06/09/2016 23:35
1 | 2 | Sepideh Asadi | h1. Skype Meeting 06092016 |
---|---|---|---|
2 | 15 | Karine Even Mendoza | *Generally discussed in the meeting* |
3 | 16 | Karine Even Mendoza | |
4 | 15 | Karine Even Mendoza | - Benchmarks |
5 | 15 | Karine Even Mendoza | - Testing of last changes in opensmt |
6 | 15 | Karine Even Mendoza | - Refinement |
7 | 15 | Karine Even Mendoza | - UF encoding |
8 | 15 | Karine Even Mendoza | - Cprover upgrade |
9 | 16 | Karine Even Mendoza | |
10 | 3 | Sepideh Asadi | |
11 | 4 | Sepideh Asadi | *Updates of current tasks:* |
12 | 3 | Sepideh Asadi | |
13 | 11 | Sepideh Asadi | Antti: works on incrementality- added some bugs to Issue-tracking |
14 | 3 | Sepideh Asadi | |
15 | 9 | Sepideh Asadi | Karine: is working on new version of CBMC- and refinement. |
16 | 3 | Sepideh Asadi | |
17 | 10 | Sepideh Asadi | Sepideh: is doing experiments on FF-HF-CBMC |
18 | 10 | Sepideh Asadi | sepideh has found some benchmarks that CBMC gets out of memory, but HiFrog and Funfrog managed to do verification very quickly. |
19 | 10 | Sepideh Asadi | Benchmarks: EvenOdd.c, Arith.c, in recursion directory |
20 | 1 | Sepideh Asadi | |
21 | 12 | Sepideh Asadi | reports some bugs: rec4.c in 17_recursion which HIfrog failed with this error:; Error: Clause has no color (triggered at PGInterAux.C, 218) |
22 | 12 | Sepideh Asadi | |
23 | 7 | Sepideh Asadi | |
24 | 8 | Sepideh Asadi | ========================================= |
25 | 8 | Sepideh Asadi | |
26 | 3 | Sepideh Asadi | *Things we agreed to do this week:* |
27 | 1 | Sepideh Asadi | |
28 | 9 | Sepideh Asadi | |
29 | 6 | Sepideh Asadi | Antti: Uploaded the benchmark of Milano guys, FABRIZIO PASTORE,(also will upload more) |
30 | 3 | Sepideh Asadi | |
31 | 3 | Sepideh Asadi | |
32 | 3 | Sepideh Asadi | Karine: |
33 | 13 | Karine Even Mendoza | 1. Upload some of SIR benchmarks |
34 | 13 | Karine Even Mendoza | 2. Refinement - checking + reporting bugs |
35 | 13 | Karine Even Mendoza | 3. Continue update cprover/cbmc 5.5 |
36 | 13 | Karine Even Mendoza | 4. Generally check hifrog with LRA after the last changes in opensmt |
37 | 13 | Karine Even Mendoza | ==> There are some bugs, I added comments and will open a new ticket if needed |
38 | 13 | Karine Even Mendoza | 5. Test refinement - #3488 issue number, several problems |
39 | 13 | Karine Even Mendoza | ==> Added a comment with the smt encoding we are sending to the solver |
40 | 14 | Karine Even Mendoza | 6. To check if it is the same ptref - check the field - PTRef::x |
41 | 14 | Karine Even Mendoza | ==> Added it to the prints + some testing. Need to test it with the original benchmark that causes the bug |
42 | 13 | Karine Even Mendoza | 7. Check the reason for improvement |
43 | 13 | Karine Even Mendoza | 7.1 funfrog - hifrog check |
44 | 13 | Karine Even Mendoza | 7.2 opensmt - opensmt2 check |
45 | 13 | Karine Even Mendoza | 8. Open new branch EUF in two weeks + start working on UF encoding (Theory.h in opensmt). |
46 | 9 | Sepideh Asadi | |
47 | 6 | Sepideh Asadi | Sepideh: |
48 | 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. |
49 | 6 | Sepideh Asadi | 2) she will do experiment on Milano guys' benchmark. |
50 | 9 | Sepideh Asadi | 3) benchmarking the OpenSMT2 incrementality implementation |
51 | 7 | Sepideh Asadi | |
52 | 7 | Sepideh Asadi | -------------- |
53 | 7 | Sepideh Asadi | We need to have proper benchmark for interpolation. |