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