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