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] Feedback on presenting Formal Methods
- Subject: [Frama-c-discuss] Feedback on presenting Formal Methods
- From: dmentre at linux-france.org (David MENTRE)
- Date: Mon, 17 May 2010 15:00:12 +0200
Hello, A few months ago, I asked for help in classifying Formal Methods in order to present them. I received two very constructive off-list answers. I've been asked (by a reader of one of those lists) to report about the final classification I used. Due to company restriction I cannot publish my slides however I can outline their content. I divided my presentation into four main parts: * Abstract Analysis (Astr?e, Frama-C, Polyspace); * Model checking (SPIN, Scade, ...); * Hoare Logic (B Method, Frama-C, ...); * Interactive Theorem Proving (Coq, PVS, Isabelle, ...). For each part, I tried to succinctly present the main objectives and advantages of the presented domain (real code analysis for Abstract analysis, temporal properties for Model checking, ...) and give a success story showing how the approach can be interesting (Astr?e for Abstract analysis, compcert for Interactive theorem proving, ...). Then, I followed a grid of several points to present the approach, keeping in mind a very practical point of view (e.g. showing examples and screen copies of tools): * Suitable domains / Possible issues * Level of expertise: how the user should be skilled. * Level of intervention: hand made model, source code, ... * Development cycle coverage / Fidelity: where in the Development cycle. How to match with real code. * Tool availability / Automatism level: are tools available? Automatic ones? * Expressiveness: What can be expressed with the considered formalism (e.g. temporal properties with model checking) I would like to publicly thank lists' readers that helped me with ideas and material. Sincerely yours, david  http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2010-March/001835.html  Yes, I know, Frama-C is as an Abstract Analysis tool as a Hoare logic proving tool with Jessie plugin. But it reflected my own usage and perception of tools availability.
- Prev by Date: [Frama-c-discuss] Small function on buffer doesn't verify
- Next by Date: [Frama-c-discuss] question about a simple example and jessie
- Previous by thread: [Frama-c-discuss] ANN: cil-0.0.1
- Next by thread: [Frama-c-discuss] Value analysis and approximaitons