--- layout: fc_discuss_archives title: Message 25 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Verification conditions left unproven by automatic prover



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