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] French slides to present Frama-C, value analysis and Jessie
- Subject: [Frama-c-discuss] French slides to present Frama-C, value analysis and Jessie
- From: STEPHANE.DUPRAT at atosorigin.com (DUPRAT Stephane)
- Date: Tue, 1 Feb 2011 11:09:22 +0000
- In-reply-to: <AANLkTikQfC8Xz4x1CMP=XES-e7a=t-QB8WG1R5Xhex75@mail.gmail.com>
Hello, Thanks for this return of experience. If it helps, here's my point of view about these remarks, which are from the side of an industrial user. > -----Message d'origine----- > De : frama-c-discuss-bounces at lists.gforge.inria.fr > [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] De la > part de David MENTRE > Envoy? : mardi 1 f?vrier 2011 09:39 > ? : Frama-C public discussion > Objet : Re: [Frama-c-discuss] French slides to present > Frama-C, value analysis and Jessie > > Hello Benjamin, > > 2011/2/1 MONATE Benjamin 205998 <Benjamin.MONATE at cea.fr>: > > Thanks a lot for making your slides available: they provide > a nice and precise overview of two plugins of Frama-C. > > Thanks. > > > What kind of remarks/questions did you get? > > Regarding Value analysis (also presented in another lesson): > mostly questions regarding lack of precision on values, > especially regarding loops (and "all programs are loops", > quoting a participant). I talked about the skein analysis in > Value analysis tutorial which is able to provide some > interesting result and the use of -slevel. But I lack first > hand practice on applying value analysis to large code. Is it > a real issue on control code, for example? Applying value analysis on the whole code of a large project is a strategy with very added-value, but the process could be very long and is not always a well controlled activity regarding the costs. It depends a lot of the analysed program. An other strategy for industrial (or not) developpers is to apply value analysis on sub-components of the program during its development. This strategy is possible thanks to the ACSL language that is able ot replace external component by their formal specification (in a restricted way, for the moment). On the other hand, size of the subcomponents that are smallers make the analysis easier and faster. It is thus possible to work in an iterative way. I'm personnaly convinced that use of value analysis is 1/ possible and 2/ adapted to different contexts and not only those of industrial and critical software. > > Regarding Jessie: "annotations have the same size as code!" > and "what about error in annotations?". For the former > remark, I could only tell that this was the price to pay to > be able to *prove* code in all its generality. Regarding the > latter remark, I told it would not be possible to prove the > goals, but a was lacking convincing arguments. > One of the attendee followed a lesson on code proof using a > functional approach and PVS powerful tactics made by a > researcher at INRIA Rennes (Thomas Genet) and told the > approach was more powerful and simple. I answered that the > discussion between the two approaches is still on-going. :-) About the remark about the size of annotation: Deductive proof is made for functional verification that are traditionnaly made by tests. And we have to know that tests are larger thant source code. And formal specification are smaller thant tests scripts. For the second remark, formal specification are specification that need a review. We have to be care in case of using a lot of axiomatic and complex formal specification. > > Overall, I already asked for it but having some examples (or > better an article that could be cited!) detailing how Frama-C > is applied on some industrial code (size of code, most > important issues and approaches used to work around them, > results obtained) would be very useful. I will try to export more concrete exemple. Regards, Stephane > > Sincerely yours, > 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 > > -- ----------------------------------------------- Stephane DUPRAT Innovation et Bureau m?thode R?gion Midi-Pyr?n?es - Agence de Toulouse 6 Impasse Alice Guy B.P. 43045 31024 - Toulouse Cedex 03 T?l : 05 34 36 32 78 Fax : 05 34 36 31 00 mailto :stephane.duprat at atosorigin.com ======================================================================= Ce message electronique est confidentiel. Il peut contenir des informations protegees par le secret professionnel, le secret de fabrication ou autres regles legales. Si vous recevez ce message par erreur, il vous est interdit de le reproduire ou de le distribuer en tout ou en partie, ou de le divulguer de quelque maniere que ce soit a quelque personne que ce soit. Nous vous prions de bien vouloir en informer Atos Origin, par telephone ou par retour d'e-mail puis de detruire le message et toutes copies de votre systeme informatique. Le contenu de ce message ne reflete pas necessairement ni les opinions d'Atos Origin ni celle des membres de son groupe. Bien que l'emetteur de ce message ait fait tout son possible pour maintenir son systeme informatique sans virus, il ne peut garantir que cette transmission ne comporte aucun virus et il ne pourra etre tenu pour responsable de quelque dommage que ce soit resultant de la transmission d'un virus. ======================================================================= This electronic transmission is confidential. It may contain information that is covered by legal professional privilege, work product immunity or other legal rules. If you have received this transmission in error, you must not copy or distribute this message or any part of it or otherwise disclose its contents to anyone. Please notify Atos Origin Legal Services by telephone or return E-mail, and then delete this transmission and any copies of it from your computer system. The views expressed in this electronic transmission do not necessarily reflect those of Atos Origin SA or any member of its group. Although the sender endeavours to maintain a computer virus free network, the sender does not warrant that this transmission is virus free and will not be liable for any damages resulting from any virus transmitted. ======================================================================= ________________________________ Ce message et les pi?ces jointes sont confidentiels et r?serv?s ? l'usage exclusif de ses destinataires. Il peut ?galement ?tre prot?g? par le secret professionnel. Si vous recevez ce message par erreur, merci d'en avertir imm?diatement l'exp?diteur et de le d?truire. L'int?grit? du message ne pouvant ?tre assur?e sur Internet, la responsabilit? du groupe Atos Origin ne pourra ?tre recherch?e quant au contenu de ce message. Bien que les meilleurs efforts soient faits pour maintenir cette transmission exempte de tout virus, l'exp?diteur ne donne aucune garantie ? cet ?gard et sa responsabilit? ne saurait ?tre recherch?e pour tout dommage r?sultant d'un virus transmis. This e-mail and the documents attached are confidential and intended solely for the addressee; it may also be privileged. If you receive this e-mail in error, please notify the sender immediately and destroy it. As its integrity cannot be secured on the Internet, the Atos Origin group liability cannot be triggered for the message content. Although the sender endeavours to maintain a computer virus-free network, the sender does not warrant that this transmission is virus-free and will not be liable for any damages resulting from any virus transmitted.
- Follow-Ups:
- [Frama-c-discuss] French slides to present Frama-C, value analysis and Jessie
- From: dmentre at linux-france.org (David MENTRE)
- [Frama-c-discuss] French slides to present Frama-C, value analysis and Jessie
- From: Dillon.Pariente at dassault-aviation.com (Pariente Dillon)
- [Frama-c-discuss] French slides to present Frama-C, value analysis and Jessie
- References:
- [Frama-c-discuss] French slides to present Frama-C, value analysis and Jessie
- From: dmentre at linux-france.org (David MENTRE)
- [Frama-c-discuss] French slides to present Frama-C, value analysis and Jessie
- Prev by Date: [Frama-c-discuss] French slides to present Frama-C, value analysis and Jessie
- Next by Date: [Frama-c-discuss] French slides to present Frama-C, value analysis and Jessie
- Previous by thread: [Frama-c-discuss] French slides to present Frama-C, value analysis and Jessie
- Next by thread: [Frama-c-discuss] French slides to present Frama-C, value analysis and Jessie
- Index(es):