Blog

Tag Archives: value

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

Results are in
Pascal Cuoq on 24 July 2012

A contest and a self-pitying lament John Regehr was organizing a craziest undefined behavior contest and the results are in. I had an entry in the contest but I did not win. My entry apparently was too obviously dangerous. As John puts it “I would have expected a modern C...

Read More