Tag Archives: facetious-colleagues

Crediting where credit is due
Pascal Cuoq on 6 September 2012

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 More

Technical interlude
Pascal Cuoq on 23 August 2012

The 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 More

To finish on termination
Pascal Cuoq on 8 June 2012

Enthusiastic 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 More

Iterating over the AST
Virgile Prevosto on 21 May 2012

Context 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 More

But wait! There may be more!
Pascal Cuoq on 14 March 2012

My 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