Алгоритм по автоматизации генерации Acsl-спецификаций, где можно найти примеры?

Question

[razexqq]

Как проходит автоматизация данных спецификаций путем применения плагинов на Frama-C.