Frama-C 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 MoreThis 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 MoreThis 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 More