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 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 MoreEnthusiastic reactions to the previous post about verifying the termination of a C program with Frama-C's value analysis lead me to write this post-scriptum. On detecting both termination and non-termination The scheme I outlined in the previous post can only confirm the termination of the program. If the program does...
Read MoreContext A facetious colleague who claims that he should be better writing his thesis but keeps committing Coq and OCaml files on Frama-C's repository, asked me the following question: Is there a function in Frama-C's kernel that can fold[1] a function over all types that appear in a C program?...
Read MoreMy colleague Boris Yakobowski is on holidays, and while leisurely browsing the internet, he seems to have stumbled upon my previous post. He e-mailed me about it. For some reason, it does not feel right to provide much biography when mentioning facetious colleagues perhaps because it would look too self-congratulatory...
Read More