The Coq mailing list

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

Hello,

This question is not strictly related to Frama-C and Coq but readers
of this list might have a good advice: does anybody know a
classification/taxonomy of various formal methods? I googled and
looked at various Wiki and web sites but found nothing very
conclusive.

I plan to do a broad presentation of formal methods and associated
tools (amongst them Frama-C and Coq) and I would like to show how
approaches like Coq, B Method, Synchronous languages, Frama-C, SAT
solvers, model checkers, etc. compare to each other.

Until now, the classification I found is between:
 * Formal Specification
 * Formal Verification
 * Formal Synthesis
with an overlap between the three sets.

Classification for software verification:
 * Axiomatic Semantics (Hoare & Co.)
 * Abstract Interpretation
 * Model Checking
 * Type Systems

Many thanks in advance for any tips,
Best regards,
david