Если вы имеете в виду «инвариант» в самом широком смысле, поскольку используется связанная страница с Daikon, то работу многих инструментов статического анализа можно описать как «обнаружение инвариантов», но, возможно, не те выразительные инварианты, которые вы искали .
Анализ значений Frama-C накапливает свои результаты, возможные значения всех переменных, для каждого оператора. Таким образом, в конце анализа он может представить нереляционную информацию об изменении домена каждой переменной в программе для каждого оператора. В на этом скриншоте инвариант состоит в том, что S всегда равно 0, 1, 3 или 6 непосредственно перед выбранной инструкцией для всех выполнений этой детерминированной программы.
Два скрытых параметра в вашем вопросе - это форма инвариантов, которые вас интересуют, и форма программ, для которых вы хотите найти эти инварианты. Например, SLAM, упомянутый в ответе Иры, был разработан для работы с кодом драйвера устройства и для вывода инвариантов, которые просто содержат необходимую информацию для проверки правильности использования системных API. Еще один инструмент, Astrée , известен тем, что отлично справляется с выводом правильных инвариантов для демонстрации безопасности программного обеспечения для управления полетом во время выполнения.
Две степени свободы создают очень большое пространство для дизайна. Вы не найдете ничего, что работает для всех видов программ на C и выведет все инварианты, которые вас могут заинтересовать, но если вы уточните свой вопрос для конкретных областей применения и типов инвариантов, у вас будет больше шансов найти соответствующие ответы.