Frama-C Comparing static analysis tools is (still) difficult Earlier this year of 2012, some of my colleagues and I took the opportunity to point out that, as a research community, we are not doing a satisfactory job of comparing static analysis tools. This article and blog post were concerned with independent...
Read MoreIn recent posts I have shown that Frama-C's value analysis could answer many reachability questions and some questions that weren't originally phrased as reachability questions about the programs in the RERS competition. If you are vaguely familiar with the internals of Frama-C's value analysis and if you tried analyzing some...
Read MoreThe current series of posts is pretty technical, huh? Here is a refreshing diversion in the form of a technical post that also touches on existential questions. What is this blog for? We don't know. Best solutions, or solutions anyone could have found If you have been following the current...
Read MoreIn the context of the RERS 2012 competition the previous post points out that value analysis option -obviously-terminates can be used to prove the termination of an instrumented program created such that its termination implies that the property (F oW) is true of the original competition program. Unfortunately this only...
Read MoreThis third installment discusses the diagnosis of liveness properties of particular C programs, using Frama-C's value analysis, for the RERS 2012 competition. [Note added in September 2012: the diagnostic found for the example in this post disagrees with the diagnostic found later and sent to the competition organizers. I am...
Read More