Данная статья является адаптированным переводом моей статьи: Formalization of code in Coq - tactics, написанной в период работы над проектом coq-tezos-of-ocaml. Суть проекта: часть исходного кода протокола криптовалюты Tezos была переведена на Coq, а затем верифицирована с помощью математических методов и…
Это обзорная статья, в которой очень поверхностно и не подробно рассказывается о том, что такое формальная верификация программного кода, зачем она нужна и чем она отличается от аудита и тестирования. Формальная верификация — это доказательство с использованием…
Продолжаем серию статей о CAP-теореме и языке Coq. В предыдущей части мы детально проанализировали определения CAP-теоремы, готовясь к её формализации на языке Coq, и нашли там серьёзную ошибку (теперь будет о чём поговорить при случае на system design interview).В этой статье мы познакомимся с основами языка Coq и для практики формализуем небольшой фрагмент геометрической системы, близкой к евклидовой. Читать далее
Привет Хабр! В этой статье я хочу поговорить о достаточно мало рассматриваемой теме анализа кода систем повышенной надежности. На хабре много статей о том, что такое хороший статический анализ, но в этой статье я бы хотел рассказать о том, что такое формальная верификация кода, а также объяснить опасность бездумного применения статических анализаторов и стандартов кодирования. Читать дальше →