--- layout: post author: Pascal Cuoq date: 2012-09-06 06:25 +0200 categories: facetious-colleagues link rers2012 format: xhtml title: "Crediting where credit is due" summary: --- {% raw %}

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 Liveness Checking as Safety Checking. I had read the article and the instrumentation I described was inspired by it but I wasn't sure I understood the article well enough to claim that I was using exactly Biere Artho and Schuppan's idea. It turns out I was pretty much.

{% endraw %}