Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Using Coq as prover

Hi Matthias,

>> In other words, just start working with native:coq and hope for the best!

We will do our best to ease the transition :-)

Just to complete previous answers, we actually plan to make the why3 coq backend also working from WP, as a replacement for the current "native:coq" one.
Since the why3 translation to Coq is a bit different than our native backend, your scripts will need some refactoring, but the proof skeletons shall be preserved.

However, I would just mention that Coq proof obligations generated by weakest precondition calculus are intrinsically difficult to master, especially when the memory model is involved. Interestingly, it is often the case where you only need the power of Coq to solve a problem that is *not* related to C-code, but that is related to some arithmetic or mathematical problem (and that remains out-of-reach from SMT solvers).

In such a case, I would recommend the following alternative :

1. Write a Why3 theory where the necessary types, symbols and their properties are stated
2. Prove the necessary lemmas in Why3, perhaps using Coq on the most tricky parts
3. Use a WP driver to bind your Why3 theory to abstract ACSL symbols, that you can now use within your code annotations.

The additional benefit of this strategy is that you can you use all the Why3 structuring facilities (theory, module, cloning) and all its libraries, without rewriting them at the ACSL level.
Notice also that we are working on making point 3 fully automated in a near future :-)

Regards, L.