Blog

Tag Archives: benchmarks

On writing a dedicated model-checker for the RERS competition
Pascal Cuoq on 24 August 2012

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

Technical interlude
Pascal Cuoq on 23 August 2012

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

Proving (F oW) true or false: alternative method
Pascal Cuoq on 22 August 2012

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

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

This 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

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