--- layout: fc_discuss_archives title: Message 91 from Frama-C-discuss on October 2013 ---
[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.