Meeting 17-22102016 - Work plan and future work » History » Version 16
Antti Hyvärinen, 20/10/2016 16:41
| 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 | 14 | Karine Even Mendoza | 1. Incremental SMT for funfrog (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 | 14 | Karine Even Mendoza | 6. Unbounded MC |
| 17 | 1 | Karine Even Mendoza | |
| 18 | 11 | Karine Even Mendoza | |
| 19 | 8 | Karine Even Mendoza | h2. Work Plan |
| 20 | 9 | Karine Even Mendoza | |
| 21 | 8 | Karine Even Mendoza | TODO |
| 22 | 6 | Karine Even Mendoza | |
| 23 | 3 | Karine Even Mendoza | h3. Tasks for OpenSMT2 |
| 24 | 3 | Karine Even Mendoza | |
| 25 | 16 | Antti Hyvärinen | - Theory combination for UF + LRA |
| 26 | 16 | Antti Hyvärinen | - Fix the code computing models |
| 27 | 3 | Karine Even Mendoza | |
| 28 | 3 | Karine Even Mendoza | |
| 29 | 3 | Karine Even Mendoza | h3. Tasks for HiFrog |
| 30 | 5 | Karine Even Mendoza | |
| 31 | 10 | Karine Even Mendoza | - Implement the algorithm for explain the error trace (the paper Grigory sent several weeks ago) |
| 32 | 1 | Karine Even Mendoza | |
| 33 | 12 | Karine Even Mendoza | - Incrementality of solver: use pop during the verification process (pop assert or pop partition) |
| 34 | 5 | Karine Even Mendoza | |
| 35 | 11 | Karine Even Mendoza | - Debug of the error trace (HiFrog and OpenSMT2) |
| 36 | 11 | Karine Even Mendoza | |
| 37 | 5 | Karine Even Mendoza | - Update of the CProver framework to 5.4 |
| 38 | 11 | Karine Even Mendoza | |
| 39 | 11 | Karine Even Mendoza | - Merge (gradually) the prop version with HiFrog dev branch |
| 40 | 15 | Karine Even Mendoza | |
| 41 | 15 | Karine Even Mendoza | - Benchmark |