Здравствуйте!

Возможно кто-нибудь видел это — http://frama-c.cea.fr/ — статический анализатор С-кода и доказательство его свойств. Что скажете?
Интересует возможность практического применения.