Frama-C news and ideas

To content | To menu | To search | Frama-C Home

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.