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] Newbie question
- Subject: [Frama-c-discuss] Newbie question
- From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
- Date: Wed, 11 Nov 2009 10:08:34 +0100
- References: <100653.83040.qm@web110603.mail.gq1.yahoo.com>
Hello again, > I am a C developer who is interesting in writing code that can be verified. > I am on Linux and it looks like only a selected number of proof assistants > are available on this platform. > It sounds to me as though Coq would be the best one. As someone who doesn't really practice automated proof but works within miles of plethora of people who do, I can give you some pretty good large-scale advice: * Coq, as you noticed, is a proof assistant, not an automatic prover. It holds your hand while you do the proof, or rather, you hold its hand. It's like walking alongside a toddler, without the warm fuzzy feeling. * Automated proof is a fascinating field with a lot of active research (and developments) being done. Each prover has some properties for which it does better than the others. Install as many of them as your religion allows you. If you don't mind the restrictive licenses that prevent them from being packages in your distribution, install Z3 (under wine) and Simplify in addition to Alt-Ergo. Some people have even gotten Why to use several versions of the same prover, because even those did not have the same strengths and weaknesses: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-September/001404.html > Do you run frama-c on Linux? The majority of Frama-C developers use Linux. Actually, none of them does not boot some sort of Unix at least once in a while. > If Coq is the way to go, is there some sort of gentle introduction > on how to use Coq with Frama-c? Learning Coq at this point would be a diversion from your original goal. While you would probably find it very interesting, building expertise in the use of automatic provers and the ways these can be helped when they fail, would be more rewarding in the short term. If you look at existing proofs of programs (does someone collect these somewhere? Here's a neat example anyway: http://why.lri.fr/queens/slides-pp.pdf ) you will see that weaknesses are often circumvented by the addition of a lemma that guides the automatic prover The lemma can later be itself proved automatically. You need some intuition of how the provers work to be able to do this, because they are typically not good at giving feedback. But experience shows that it is possible to build such working knowledge even with limited expertise of the theoretical ramifications. Our colleagues at FIRST (they read this list) have a draft of a document titled "ACSL by example", which contains functions, with formal specifications, that have been formally verified. Perhaps they will agree to show you a draft of this document. Pascal
- References:
- [Frama-c-discuss] Newbie question
- From: hxdg21 at yahoo.com (Aaron Rocha)
- [Frama-c-discuss] Newbie question
- Prev by Date: [Frama-c-discuss] Newbie question
- Next by Date: [Frama-c-discuss] Frama-C vs Ada/SPARK
- Previous by thread: [Frama-c-discuss] Newbie question
- Next by thread: [Frama-c-discuss] Newbie question
- Index(es):