Frama-C 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 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 MoreThe 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 MoreACSL There were quite a few posts recently that were concerned with ACSL, and a few more are planned for the near future. ACSL is a specification language for C (comparable with JML for Java, for those who know about JML). Some people call it a BISL, for “Behavioral Interface...
Read MoreSome time ago, we saw that in C arrays and pointers have some subtle differences. A facetious colleague just remarked that this is also the case in ACSL especially if you use the \at(e L) construction which basically says that e is supposed to be evaluated in the state when...
Read More