Существует ли инструмент статического обнаружения инвариантов для программ на языке Си?

Я ищу инструмент, который может статически обнаруживать инварианты в программах на языке Си. Я проверил Daikon , но он обнаруживает инварианты только динамически.

Есть ли инструмент для того, что я ищу? Спасибо!