Meeting 17-22102016 - Work plan and future work¶

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?

Work Plan¶

TODO

Tasks for OpenSMT2¶

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