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



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>