--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on March 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Off-topic] Classification/taxonomy of formal methods?



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