A Foundation for Flow-Based Program Matching Using Temporal Logic and
Model Checking

Julia Lawall, Inria

Coccinelle is a program matching and transformation tool for C code,
founded on the notion of a semantic patch, in which matching and
transformation specifications are expressed using a patch-like syntax.
Coccinelle has been extensively used for bug finding and evolution in the
context of the Linux kernel, and other C software.  In this talk, we
provide an overview of Coccinelle and its use on Linux code, as well as
describing its internal design, based on a novel variant of the temporal
logic CTL.

This is joint work with Julien Brunel, Damien Doligez, Rene Rydhof Hansen,
and Gilles Muller