Crediting where credit is due
By pascal on Thursday, September 6 2012, 07:25 - Permalink
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.