--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on March 2010 ---
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