Crediting where credit is due

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.