Meeting 17-22102016 - Work plan and future work » History » Version 12
Karine Even Mendoza, 20/10/2016 15:50
1 | 1 | Karine Even Mendoza | h1. Meeting 17-22102016 - Work plan and future work |
---|---|---|---|
2 | 1 | Karine Even Mendoza | |
3 | 1 | Karine Even Mendoza | |
4 | 7 | Karine Even Mendoza | h2. Future work: |
5 | 7 | Karine Even Mendoza | |
6 | 12 | Karine Even Mendoza | 1. Use incrementalitly of opensmt2 in hifrog (efficiency or more precise summary) |
7 | 2 | Karine Even Mendoza | |
8 | 2 | Karine Even Mendoza | 2. Fault explain/localize on the error trace |
9 | 3 | Karine Even Mendoza | |
10 | 4 | Karine Even Mendoza | 3. Theory aware MC for FunFrog + OpenSMT2 |
11 | 4 | Karine Even Mendoza | |
12 | 11 | Karine Even Mendoza | 4. Combination of theory (E.g., using UF and encoding some part in LRA if not precise enough) |
13 | 1 | Karine Even Mendoza | |
14 | 11 | Karine Even Mendoza | 5. Can we do something with parallel solver? |
15 | 3 | Karine Even Mendoza | |
16 | 1 | Karine Even Mendoza | |
17 | 11 | Karine Even Mendoza | |
18 | 8 | Karine Even Mendoza | h2. Work Plan |
19 | 9 | Karine Even Mendoza | |
20 | 8 | Karine Even Mendoza | TODO |
21 | 6 | Karine Even Mendoza | |
22 | 3 | Karine Even Mendoza | h3. Tasks for OpenSMT2 |
23 | 3 | Karine Even Mendoza | |
24 | 3 | Karine Even Mendoza | |
25 | 3 | Karine Even Mendoza | |
26 | 3 | Karine Even Mendoza | h3. Tasks for HiFrog |
27 | 5 | Karine Even Mendoza | |
28 | 10 | Karine Even Mendoza | - Implement the algorithm for explain the error trace (the paper Grigory sent several weeks ago) |
29 | 1 | Karine Even Mendoza | |
30 | 12 | Karine Even Mendoza | - Incrementality of solver: use pop during the verification process (pop assert or pop partition) |
31 | 5 | Karine Even Mendoza | |
32 | 11 | Karine Even Mendoza | - Debug of the error trace (HiFrog and OpenSMT2) |
33 | 11 | Karine Even Mendoza | |
34 | 5 | Karine Even Mendoza | - Update of the CProver framework to 5.4 |
35 | 11 | Karine Even Mendoza | |
36 | 11 | Karine Even Mendoza | - Merge (gradually) the prop version with HiFrog dev branch |