Формальная верификация и ассистенты доказательств

Формальная верификация с помощью машинной проверки математических доказательств устанавливает, что программное обеспечение соответствует своей спецификации; ассистенты доказательств — это инструменты, которые создают и проверяют такие доказательства.

Definition

Формальная верификация — это построение строгого, машинопроверяемого доказательства того, что система удовлетворяет формальной спецификации, а ассистент доказательств — это программное обеспечение, которое помогает пользователю разрабатывать такие доказательства и механически проверять их достоверность.

Scope

Эта тема охватывает дедуктивную верификацию и интерактивное доказательство теорем: ассистенты доказательств, основанные на теории типов или логике высшего порядка (такие как Coq, Isabelle, Lean и Agda), подход LCF к надёжным доказательствам, основу «предложения как типы», автоматизацию доказательств и тактики, а также знаковые верифицированные артефакты, включая компиляторы и ядра операционных систем.

Core questions

• Как можно доказать и машинным способом проверить полную функциональную корректность?
• Почему ассистенты доказательств заслуживают доверия, и что такое доверенная вычислительная база?
• Как соответствие Карри-Ховарда связывает доказательства и программы?
• Что требуется для верификации реальных систем, таких как компиляторы и ядра?

Key theories

Подход LCF к надёжным доказательствам

Edinburgh LCF Гордона, Милнера и Уодсворта представил небольшое доверенное ядро доказательств, через которое должны проходить все теоремы, так что даже сложная автоматизация не может привести к некорректным доказательствам.

Верифицированный компилятор (CompCert)

CompCert Леруа — это компилятор языка C, корректность которого доказана с помощью ассистента доказательств, с машинопроверяемой теоремой о том, что сгенерированный код уточняет семантику исходной программы.

Верифицированное ядро операционной системы (seL4)

Кляйн и его коллеги создали машинопроверяемое доказательство функциональной корректности для микроядра seL4, демонстрируя сквозную верификацию низкоуровневого системного программного обеспечения.

Clinical relevance

Механизированная верификация обеспечивает высочайший уровень надёжности для критически важного программного обеспечения, позволяя создавать компиляторы, ядра и криптографические библиотеки с доказанными гарантиями, а не с уверенностью, основанной на тестировании. Ассистенты доказательств также всё чаще используются для формализации самой математики.

History

Интерактивное доказательство теорем началось с Edinburgh LCF в 1970-х годах, чей метаязык ML и доверенное ядро сформировали последующие системы. Ассистенты, основанные на теории типов, такие как Coq и Agda, и системы логики высшего порядка, такие как Isabelle/HOL, развивались в последующие десятилетия, кульминацией чего стали знаковые верифицированные артефакты: компилятор CompCert (2009) и ядро seL4 (2009).

Debates

Стоимость верификации против полученной надёжности

Создание машинопроверяемых доказательств для больших систем требует огромных усилий, что вызывает дебаты о том, где полная верификация оправдана, а где достаточно более лёгких методов, и насколько можно автоматизировать доказательства.

Key figures

• Robin Milner
• Michael Gordon
• Xavier Leroy
• Gerwin Klein
• Robert Harper

Seminal works

• gordon1979
• leroy2009
• klein2009
• harper2016

Frequently asked questions

Что такое ассистент доказательств?

Ассистент доказательств — это программное обеспечение, в котором пользователь интерактивно строит формальные доказательства, в то время как система механически проверяет каждый шаг, так что завершённое доказательство надёжно вплоть до небольшого, тщательно проверенного ядра.

Чем верификация программы отличается от её тестирования?

Тестирование проверяет поведение на выбранных входных данных и может только выявить наличие ошибок, в то время как формальная верификация доказывает корректность для всех входных данных, разрешённых спецификацией, устанавливая отсутствие указанных ошибок.