8 апреля 2025 г.
«Формальная верификация алгоритмов: применение системы Coq для метода прогонки»
Аннотация доклада.
Формальная верификация позволяет математически доказать корректность программного обеспечения, повышая его надежность в критически важных системах. В докладе рассматриваются основные подходы к формальной верификации, их преимущества и ограничения. Особое внимание уделено применению системы Coq на примере доказательства корректности алгоритма решения систем линейных уравнений. Также обсуждаются трудности практического использования формальной верификации и возможные пути их преодоления.