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