Frama-C Perry E. Metzger takes a look at formal verification [removed dead link]. This is good stuff; there is a lot to agree with here. However agreeing with Perry's post alone would not make a very interesting counterpoint. If agreeing was the only thing I intended to do I might even...
Read MoreThere is a C quiz in the middle of this post, lost in the middle of all the reminiscing. A history of arithmetic overflows in Frama-C From the very beginnings in 2005, until after the first Open Source release in 2008, Frama-C's value analysis was assuming that all arithmetic overflows...
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 previous post links to a message [removed dead link] from Michał Moskal highlighting ACSL constructs that the VCC developers at Microsoft Research had either regretted the absence of or found superfluous while re-designing their own annotation language for VCC. In that e-mail the third item in the “missing” list...
Read MoreI have just sent a list of changewishes (1 2) to a static analysis competition mailing-list and that reminded me of a blog post I had to write on the strictness of the type-checker in upcoming Frama-C release Oxygen. This is the blog post. This post is not about uninitialized...
Read More