Frama-C In a recent post I showed how to use Frama-C's value analysis to prove a particular liveness property true or false of a particular C program. My colleague Sébastien Bardin reliably informs me that the ideas for reducing a liveness property to a reachability property were all in the article...
Read MoreExtending the framework Some time ago, one of our fellow users asked us whether it was possible to extract the control-flow graph (CFG) of C functions from Frama-C. Fact is, although the CFG is computed during the elaboration of the AST, nothing exists currently to present the information to the...
Read MoreIn 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 MoreThe 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 MoreIn 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