Public announcements

Yes, I have read that static analysis post

If you are one of the three persons in the world who have not sent me a link to John Carmack's Christmas post on static analysis [removed dead link] go ahead and read it it might interest you. You can stop sending me that link now.

The post is very much a text version of the second half of his August QuakeCon keynote which I prefer if only as someone who sometimes has to speak in public for the amazing delivery. Here's some commentary on the PC-lint part of the post. I was myself going to comment on the "pursuing a Space Shuttle style code development process for game development" because the tools can be the same or at least take advantage of the same techniques and just be employed differently to answer different needs. I thought that if I only had time to put my arguments in order I might convincingly argue this and rebound on John Regehr's post by characterizing semantic static analyzers as limiting the programmer to the dialect of correct programs. But thinking about it I realize that I know nothing about game development and that it would be presumptuous to make strong claims there. In the case of Frama-C and Frama-C is not the only analyzer intended for "Space Shuttle style code" and quality objectives the total feedback we have is still limited enough to nearly double in one day and this feedback is still all about Space Shuttle style development and verification. And that day was yesterday.

U3CAT meeting

Yesterday was the day members of the national research project U3CAT gathered to tell each other about recent developments. Several presentations were on experiments done at Atos Origin SA and CS. You can't expect them to reveal too much about the actual code but yes it was Space Shuttle-like and the results are very satisfying.

One of the points that emerged was that we need to invent a word for alarms that are eventually categorized as innocuous but for which the information to classify them so was not in the source code provided to the analyzer. One actual example yesterday was the division of two values that came from sensors where Frama-C's value analysis warned that the result of the division might overflow the 16-bit int it was then stored into. Checking with the developers it turned out that specifications ensure that the values from the sensors will be such that the conversion is safe. Calling this a "false alarm" would be unfair to the analyzer since the information was not in the source code. I suggest to call this kind of alarm a "verification point". And so the bottom line of that particular experiment on a few thousand lines of C was a couple of true alarms a great many verification points and no false alarms. Apparently both the true alarms (that lead to code changes) and the verification points (that did not lead to code changes) were well received by the developers.

The thing about Atos Origin and CS is that they are service providers. They will develop and/or verify software the way you contract them to and while they may use Frama-C a little bit for software quality even if it's not in the contract they can't use it very much then. By not making Frama-C verification part of the contract you are effectively tying their hands. If on the other hand you contract them to use it as part of the development and/or verification they already have experts who can do it efficiently (and one thing I am sure both these companies are good at is internally routing tasks to employees who have the corresponding competences).

Conclusion

One wish I have for 2012 is to spend at least some of my time working on making Frama-C useful for non-Shuttle-like code. On the other hand if you are going to work on Shuttle-like code in 2012 you don't need to wait. Yesterday's meeting was another confirmation that for that purpose Frama-C is ready to be employed productively now.