Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Verification conditions left unproven by automatic prover
  • From: dmentre at linux-france.org (David MENTRE)
  • Date: Tue, 5 Nov 2013 16:38:44 +0100
  • In-reply-to: <BAY169-W18848E3211D79EFC10798197080@phx.gbl>
  • References: <BAY169-W10988CE73D54BB0035B28CE970D0@phx.gbl> <526A8DA2.7000000@inria.fr> <BAY169-W18848E3211D79EFC10798197080@phx.gbl>
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