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?

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>