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

  • Subject: [Frama-c-discuss] Verification conditions left unproven by automatic prover
  • From: x_cui at hotmail.com (Xiao-lei Cui)
  • Date: Fri, 25 Oct 2013 01:05:48 -0400
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?
   many thanks.. 


tony cui


Theory is when you know all and nothing works. 
Practice is when all works and nobody knows why. 
In this case, we have put together theory and practice: nothing works... and nobody knows why!

 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131025/5c3a82dc/attachment.html>