Tag Archives: benchmarks

Participating in the RERS 2012 competition: reachability questions
Pascal Cuoq on 20 August 2012

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 More

Understand LTL? Join us!
Pascal Cuoq on 6 August 2012

Here 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 More

Oxygen is stricter about types and why you should get used to it
Pascal Cuoq on 27 July 2012

I 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

Undefined behavior is a harsh mistress
Pascal Cuoq on 28 June 2012

Mark 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 More

Benchmarking static analyzers
Pascal Cuoq on 29 April 2012

A 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