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] Verification conditions left unproven by automatic prover


On 10/25/2013 07:05 AM, Xiao-lei Cui wrote:
> Hi All,
>    We plan to used frama-c/jessie to verify functional property of a
> small OS kernel. Many complex verification conditions are expected to be
> left unproven. In documentation, VC generated by jessie can be passed to
> interactive proving assistant, like PVS, Coq, HOL... 
>    I am new to frama-c and  have little handy experience to these
> interactive provers, knowing the basics of theorem prover though. Does
> anyone have a simple demo or tutorial showing the verification process
> that an interactive prover is used to verify VCs?

Why3 documentation has a small tutorial for getting started, including
the use of Coq.

Nevertheless, seeing the sentences

>    We plan to used frama-c/jessie to verify functional property of a
>  small OS kernel

and

>    I am new to frama-c

I'd like to recommend you to learn about Frama-C first, not only the
Jessie plugin but also others, and then decide what is the best plan for
your verify properties on your small OS kernel.