--- layout: fc_discuss_archives title: Message 24 from Frama-C-discuss on May 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-c support for dynamic memory



Hello,

as Claude Marché pointed out , Frama-C has been funded and still is funded by French public money (and EU money, I might add).

Regarding, deductive verification, there is also the AstraVer deductive verification tool chain that is 
derived from and closely related to Frama-C/Why3/Jessie (https://forge.ispras.ru/projects/astraver/wiki).

AstraVer is developed at the Institute for System Programming in Moscow, Russia (https://www.ispras.ru/en/)
and has been applied for some impressive verification work for the Linux kernel.

Regards

Jens