Meeting 17-22102016 - Work plan and future work¶

Future work:¶

1. Use incrementalitly of opensmt2 in hifrog (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?

Work Plan¶

TODO

Tasks for OpenSMT2¶

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