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

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>