Is there a static invariant discovery tool for C programs?

Question

I'm looking for a tool that can statically discover invariants in C programs. I checked out Daikon but it discovers invariants only dynamically.

Is there a tool available for what I'm looking for? Thanks!

Answer 1

See The SLAM project: debugging system software via static analysis. It claims to infer invariants statically, for just what you asked for, the C language. The author, Tom Ball, is widely known for stellar work in program analysis.

Answer 2

If you mean "invariant" in the widest sense, as the linked page to Daikon is using, then the work of many static analysis tools can be described as "discovering invariants", just perhaps not the expressive invariants you were looking for.

Frama-C's value analysis accumulates its results, the possible values of all variables, for each statement. At the end of the analysis, it can thus present non-relational information about the domain variation of each variable in the program, at each statement. In this screenshot, an invariant is that S is always 0, 1, 3 or 6 just before the selected instruction, for all executions of this deterministic program.

The two hidden parameters in your question are the shape of the invariants you are interested in, and the shape of the programs you want to find these invariants for. For instance, SLAM, mentioned in Ira's answer, was designed to work on device driver code, and to infer invariants that just contain the necessary information for verifying proper use of system APIs. Another tool, Astrée, is famous for doing a very good job at inferring just the right invariants to demonstrate runtime safety of flight control software.

The two degrees of freedom make for a very large design space. You won't find anything that works for all kinds of C programs and infers all the invariants you might be interested in, but if you refine your question for specific application domains and kinds of invariants, you will have better chances to find relevant answers.