--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on May 2020 ---
Hello Mike, hello to all, Le 18/05/2020 à 03:21, Whalen, Mike a écrit : > Hello all, > >  Apologies for perhaps an unfair criticism of the WP manual. It is > really a nice document, and I have been able to prove some interesting > things. However, if we wish to use frama-c for AWS-related projects, we > must have support for dynamic memory. Interesting to learn that AWS aims at formally verifying C code. It is of course legitimate that you investigate on the existing tools to do so. Your analysis about capabilities of Frama-C and the WP plugin seems accurate to me. Let me add a few points that may make your analysis even more informed * verifying C code involving complex data-structures, including dynamic memory allocation, remains nowadays a complex task and a complex problem that is the subject of many on-going research in academia. It is not the case that you could find a perfect tool that would suit your needs off-the-shelf * Using techniques based on deductive verification is certainly promising, however for industrial needs I think it is important to have a broader vision and be ready to use several different techniques. For example regarding using Frama-C I was wondering if you investigated the Eva plug-in and how Eva and WP can be used in combination? * a less academic point : developing verification environment like Frama-C and make them reasonably usable from an industrial perspective costs a lot of human resources and money. Frama-C and WP are freely available, their development were and are supported in part by French public funding and in part by collaborations and contracts with industrial users. Is AWS considering a collaboration with the Frama-C developer team, with corresponding funding? [Disclaimer: I'm not member of Frama-C devteam, not a member of the CEA institute... yet I am paying taxes in France...] > In looking at more of the plug-ins, it appears that Jessie is built on > top of separation logic. It is still referenced in the frama-c web > site, but is it still supported? The documentation was a bit sketchy. Being the main and almost only remaining maintainer of Jessie, I can say that they are current developments for porting it to recent Frama-C versions, but the development is now stopped due to absence of funding. Have a nice day, take care, - Claude