--- layout: fc_discuss_archives title: Message 35 from Frama-C-discuss on November 2009 ---
[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