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

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