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