--- layout: fc_discuss_archives title: Message 4 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?



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>