Meeting 17-22102016 - Work plan and future work » History » Version 10
Version 9 (Karine Even Mendoza, 20/10/2016 13:26) → Version 10/16 (Karine Even Mendoza, 20/10/2016 15:36)
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. 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
- Update of the CProver framework to 5.4
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. 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
- Update of the CProver framework to 5.4