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] New user questions
- Subject: [Frama-c-discuss] New user questions
- From: loic.correnson at cea.fr (CORRENSON Loic)
- Date: Mon, 4 May 2020 14:37:41 +0000
- In-reply-to: <4545E688-FE71-4FFA-8888-D5FF6EB15FE2@amazon.com>
- References: <D7B0F84A-CE7D-425D-B1E6-8D49FA8AFCFC@amazon.com> <86C8F6F1-0819-4A36-B0ED-AF90FAE77CD7@fokus.fraunhofer.de>, <4545E688-FE71-4FFA-8888-D5FF6EB15FE2@amazon.com>
Now, regarding a comparison against VeriFast, I would say that the most prominent difference is : - VeriFast uses separation logic to reason on pointers and aliasing - Frama-C/WP uses first-order logic with built-in separation for this purpose PROS: VeriFast is good at specifying and proving programs with complex data structures with structural separation of pointers (trees, chained lists, etc.) CONS: separation logic is difficult to work with in an automated way; VeriFast need explicit proof scripts PROS: Frama-C builtin separation makes proof obligation easy to discharge by standard SMT provers CONS: Complex memory invariants are very difficult to handle for WP Regards, L. ________________________________________ De : Frama-c-discuss [frama-c-discuss-bounces at lists.gforge.inria.fr] de la part de Whalen, Mike [mww at amazon.com] Envoyé : lundi 4 mai 2020 16:18 à : Frama-C public discussion Objet : Re: [Frama-c-discuss] New user questions Thank you very much for your help and your responses. Just to be clear, I am not looking for an editor, only a better way to debug proof failures. So far, I have not had substantial problems, but I will be looking at large code bases and I am sure will run into trouble at some point. Any strategies for debugging proofs on large codebases would be appreciated! Perhaps this begs a wider questions. What do folks on this list see as the major strengths/weaknesses of frama-c using WP/Jessie as opposed to VeriFast? Thanks again for your time, Mike On 5/2/20, 12:53 AM, "Frama-c-discuss on behalf of Gerlach, Jens" <frama-c-discuss-bounces at lists.gforge.inria.fr on behalf of jens.gerlach at fokus.fraunhofer.de> wrote: CAUTION: This email originated from outside of the organization. Do not click links or open attachments unless you can confirm the sender and know the content is safe. Hello Mike, > Finally, for debugging is there any kind of symbolic debugger or way to get counterexample information? The VeriFast tool has a nice IDE where you can forward/back-step through a program with a symbolic heap. At the moment, when a proof fails, I just stare hard at it and try to figure out how to fix it, but I would expect power-users have a few more things in their bag of tricks. The WP tutorial did not have a lot of information on this aspect. I can totally understand this feeling because I have been working (https://github.com/fraunhoferfokus/acsl-by-example) with WP for a long time and also know VeriFast very well. The truth, however, is that I got used to it. At the same time, proving is expected to require a lot of thinking which sometimes might involve staring for a long time on some snippets of code and writing tests to check whether some assumptions that one has made are really valid. In fact, Frama-C also supports the combination of formal verification and testing but other people can tell you more about this. I am not a Frama-C developer but as far as I understand, Frama-C in general and WP in particular have been originally developed for domains where safety is of utmost importance. Think of air planes and nuclear power plants. These safety-related domains are regulated by very strict system/software development processes. Quick turn-arounds or agile development have only slowly entered these domains. In particular, it is often required in these domains that during the process of verification no (accidental) code changes can occur. The simplest way to achieve this is to omit the editor in the gui of the verification tool⦠Regards Jens _______________________________________________ Frama-c-discuss mailing list Frama-c-discuss at lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss _______________________________________________ Frama-c-discuss mailing list Frama-c-discuss at lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss
- References:
- [Frama-c-discuss] New user questions
- From: mww at amazon.com (Whalen, Mike)
- [Frama-c-discuss] New user questions
- From: jens.gerlach at fokus.fraunhofer.de (Gerlach, Jens)
- [Frama-c-discuss] New user questions
- From: mww at amazon.com (Whalen, Mike)
- [Frama-c-discuss] New user questions
- Prev by Date: [Frama-c-discuss] New user questions
- Next by Date: [Frama-c-discuss] Frama/Clang Issues
- Previous by thread: [Frama-c-discuss] New user questions
- Next by thread: [Frama-c-discuss] checking Monocypher
- Index(es):