If you mean “invariant” in the broadest sense, since the linked page with Daikon is used, then the work of many static analysis tools can be described as “detecting invariants”, perhaps not the expressive invariants you were looking for.
Analysis of the value of Frama-C accumulates its results, the possible values of all variables for each statement. At the end of the analysis, he can thus represent non-relational information about the variation of the domain of each variable in the program in each expression. In this screenshot , the invariant is that S always 0, 1, 3 or 6 immediately before the selected command, for all executions of this deterministic program.
Two hidden parameters in your question are the form of the invariants you are interested in and the form of the programs for which you want to find these invariants. For example, the SLAM mentioned in Ai's answer was designed to work with device driver code and to output invariants that simply contain the necessary information to verify the correct use of system APIs. Another tool, Astrée , is famous for doing a very good job, choosing only the right invariants to demonstrate safety during flight control programs.
Two degrees of freedom make up a very large design space. You will not find anything that works for all kinds of C programs, and you will find out all the invariants that may interest you, but if you clarify your question for specific application domains and types of invariants, you will be more likely to find the corresponding answers.
source share