Meeting 17-22102016 - Work plan and future work¶

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

Work Plan¶

TODO

Tasks for OpenSMT2¶

- Theory combination for UF + LRA
- Fix the code computing models

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