The Coq mailing list

[David MENTRE <dmentre AT linux-france.org>]

Hello,

A few months ago, I asked for help in classifying Formal Methods in
order to present them[1]. I received two very constructive off-list
answers.

I've been asked (by a reader of one of those lists) to report about
the final classification I used. Due to company restriction I cannot
publish my slides however I can outline their content.

I divided my presentation into four main parts:
 * Abstract Analysis (Astrée, Frama-C, Polyspace);
 * Model checking (SPIN, Scade, ...);
 * Hoare Logic (B Method, Frama-C[2], ...);
 * Interactive Theorem Proving (Coq, PVS, Isabelle, ...).

For each part, I tried to succinctly present the main objectives and
advantages of the presented domain (real code analysis for Abstract
analysis, temporal properties for Model checking, ...) and give a
success story showing how the approach can be interesting (Astrée for
Abstract analysis, compcert for Interactive theorem proving, ...).
Then, I followed a grid of several points to present the approach,
keeping in mind a very practical point of view (e.g. showing examples
and screen copies of tools):
 * Suitable domains / Possible issues
 * Level of expertise: how the user should be skilled.
 * Level of intervention: hand made model, source code, ...
 * Development cycle coverage / Fidelity: where in the Development
cycle. How to match with real code.
 * Tool availability / Automatism level: are tools available? Automatic ones?
 * Expressiveness: What can be expressed with the considered formalism
(e.g. temporal properties with model checking)

I would like to publicly thank lists' readers that helped me with
ideas and material.

Sincerely yours,
david

[1] 
http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2010-March/001835.html

[2] Yes, I know, Frama-C is as an Abstract Analysis tool as a Hoare
logic proving tool with Jessie plugin. But it reflected my own usage
and perception of tools availability.