Meeting 17-22102016 - Work plan and future work » History » Version 11
Version 10 (Karine Even Mendoza, 20/10/2016 15:36) → Version 11/16 (Karine Even Mendoza, 20/10/2016 15:47)
h1. Meeting 17-22102016 - Work plan and future work
h2. Future work:
1. Use incrementalitly of opensmt2 in hifrog
2. Fault explain/localize on the error trace
3. Theory aware MC for FunFrog + OpenSMT2
4. Combination of theory (E.g., using UF and encoding some part in LRA if not precise enough)
5. Can we do something with parallel solver?
h2. Work Plan
TODO
h3. Tasks for OpenSMT2
h3. Tasks for HiFrog
- Implement the algorithm for explain the error trace (the paper Grigory sent several weeks ago)
- Debug of the error trace (HiFrog and OpenSMT2)
- Incrementality of solver: use pop during the verification process
- Debug of the error trace (HiFrog and OpenSMT2)
- Update of the CProver framework to 5.4
- Merge (gradually) the prop version with HiFrog dev branch
h2. Future work:
1. Use incrementalitly of opensmt2 in hifrog
2. Fault explain/localize on the error trace
3. Theory aware MC for FunFrog + OpenSMT2
4. Combination of theory (E.g., using UF and encoding some part in LRA if not precise enough)
5. Can we do something with parallel solver?
h2. Work Plan
TODO
h3. Tasks for OpenSMT2
h3. Tasks for HiFrog
- Implement the algorithm for explain the error trace (the paper Grigory sent several weeks ago)
- Debug of the error trace (HiFrog and OpenSMT2)
- Incrementality of solver: use pop during the verification process
- Debug of the error trace (HiFrog and OpenSMT2)
- Update of the CProver framework to 5.4
- Merge (gradually) the prop version with HiFrog dev branch