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] Frama-C vs Ada/SPARK

Hello,

Thank you for this detailed and interesting answer.

2009/11/12 Yannick Moy <yannick.moy at gmail.com>:
> I should add that we are in the process of plugging the Why tool for
> verifying SPARK programs, at AdaCore/Praxis, but the results of this project
> will not be available anytime soon.

Will the results be Open Source / Free Software?

> In this same project, we will be working with people from Frama-C to verify
> mixed Ada/C programs.

I would be interested to know about such results. Are the used
programs real ones or build examples? If they are real ones, from
which domain (avionics, railway, ...)?

Regards,
david