Blog
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 MoreParticipating 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 MoreUnderstand 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 Moreassume and assert Pascal Cuoq on 3 August 2012
The previous post links to a message [removed dead link] from Michał Moskal highlighting ACSL constructs that the VCC developers at Microsoft Research had either regretted the absence of or found superfluous while re-designing their own annotation language for VCC. In that e-mail the third item in the “missing” list...
Read More