--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on November 2013 ---
Hello Xiao-lei, 2013/10/28 Xiao-lei Cui <x_cui at hotmail.com>: > 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. In any case, I (and probably other readers of this list!) would be interested to have any feedback on your use of Frama-C: what did work or not, what you could prove or not, etc. Best regards, david