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] [Off-topic] Classification/taxonomy of formal methods?

  • Subject: [Frama-c-discuss] [Off-topic] Classification/taxonomy of formal methods?
  • From: dmentre at linux-france.org (David MENTRE)
  • Date: Wed, 3 Mar 2010 15:38:36 +0100
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