Skype Meeting 06092016 » History » Version 21
Sepideh Asadi, 07/09/2016 15:49
| 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 | - Testing of last changes in opensmt |
||
| 7 | - Refinement |
||
| 8 | - UF encoding |
||
| 9 | - 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 | sepideh has found some benchmarks that CBMC gets out of memory, but HiFrog and Funfrog managed to do verification very quickly. |
||
| 20 | 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 | |||
| 24 | 7 | Sepideh Asadi | |
| 25 | 8 | Sepideh Asadi | ========================================= |
| 26 | |||
| 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 | 21 | Sepideh Asadi | continuing work on incrementality on OpenSMT2 |
| 32 | 3 | Sepideh Asadi | |
| 33 | |||
| 34 | Karine: |
||
| 35 | 13 | Karine Even Mendoza | 1. Upload some of SIR benchmarks |
| 36 | 2. Refinement - checking + reporting bugs |
||
| 37 | 3. Continue update cprover/cbmc 5.5 |
||
| 38 | 4. Generally check hifrog with LRA after the last changes in opensmt |
||
| 39 | ==> There are some bugs, I added comments and will open a new ticket if needed |
||
| 40 | 5. Test refinement - #3488 issue number, several problems |
||
| 41 | ==> 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 | ==> 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 | 7.1 funfrog - hifrog check |
||
| 46 | 7.2 opensmt - opensmt2 check |
||
| 47 | 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 | -------------- |
||
| 55 | We need to have proper benchmark for interpolation. |