--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on March 2010 ---
You may want to look at http://www.cs.umd.edu/~mvz/pub/notes.pdf (I did not read it yet, so can't really give an informed opinion, but the table of contents seem reasonable) -- Yannick On Wed, Mar 3, 2010 at 3:38 PM, David MENTRE <dmentre at linux-france.org>wrote: > 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 > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100311/251fa2ed/attachment.htm>