--- layout: fc_discuss_archives title: Message 94 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



thanks for the hint. At some stage, we will need to use interactive prover for verification. we started using frama-c to document the kernel's source code two month ago. we are now evaluating the workload in the verification process. 

xiao-lei 



> Date: Fri, 25 Oct 2013 17:26:26 +0200 
> From: Claude.Marche at inria.fr
> To: frama-c-discuss at lists.gforge.inria.fr
> Subject: Re: [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.
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131027/95f90598/attachment.html>