I've talked to Yannick quite a lot in the past as my lab develops Why3 and SPARK uses my translation for their new support for pointers (access types).
Additionally, my advisor collaborates with them on counterexample generation, especially with managing to get readable counterexamples out from the SMT.
We've toyed a little with invariant generation but its very tricky to get something actually usable.
Additionally, I have the personal (soft) requirement that the generated invariant should be injected into the source code and not purely internal / hidden.
Additionally, my advisor collaborates with them on counterexample generation, especially with managing to get readable counterexamples out from the SMT. We've toyed a little with invariant generation but its very tricky to get something actually usable. Additionally, I have the personal (soft) requirement that the generated invariant should be injected into the source code and not purely internal / hidden.