Meeting 17-22102016 - Work plan and future work » History » Version 15
Version 14 (Karine Even Mendoza, 20/10/2016 16:00) → Version 15/16 (Karine Even Mendoza, 20/10/2016 16:03)
h1. Meeting 17-22102016 - Work plan and future work
h2. Future work:
1. Incremental SMT for funfrog (efficiency or more precise summary)
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?
6. Unbounded MC
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)
- Incrementality of solver: use pop during the verification process (pop assert or pop partition)
- 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
- Benchmark
h2. Future work:
1. Incremental SMT for funfrog (efficiency or more precise summary)
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?
6. Unbounded MC
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)
- Incrementality of solver: use pop during the verification process (pop assert or pop partition)
- 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
- Benchmark