Frama-C This post is a follow-up to this one. It begins to describe our participation using Frama-C's value analysis in the RERS 2012 competition. In theory The competition features nine target programs of increasing difficulty. Some of the questions to be answered about the target programs are reachability questions. This is...
Read MoreHere is yet another software verification competition. If you are a specialist of the verification of temporal properties and you have been regretting not to snatch that easy Xbox 360 (with Kinect!) in 2011* this is your chance to make up for it! We have the reachability part of the...
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 MoreMark Shroyer has discovered an interesting consequence of undefined behavior in the compiled version of a C program: a variable behaves as both true and false as a result of being uninitialized. The post is great and could not come at a better time. I needed for the talk I...
Read MoreA meta-article on benchmarking Some colleagues and I are about to submit this article on the subject of benchmarking static analyzers. Rather than another benchmark it is a list of general recommendations and pitfalls when benchmarking static analyzers. The article is illustrated on C program constructs because that's what we...
Read More