Verificação Formal e Assistentes de Prova

A verificação formal estabelece, por meio de prova matemática verificada por máquina, que o software atende à sua especificação; assistentes de prova são as ferramentas que constroem e verificam tais provas.

Definition

Verificação formal é a construção de uma prova rigorosa, verificada por máquina, de que um sistema satisfaz uma especificação formal, e um assistente de prova é um software que ajuda um usuário a desenvolver tais provas e verifica mecanicamente sua validade.

Scope

Este tópico abrange a verificação dedutiva e a prova de teoremas interativa: assistentes de prova baseados em teoria de tipos ou lógica de ordem superior (como Coq, Isabelle, Lean e Agda), a abordagem LCF para prova confiável, o fundamento de proposições-como-tipos, automação de prova e táticas, e artefatos verificados marcantes, incluindo compiladores e kernels de sistemas operacionais.

Core questions

• Como a correção funcional completa pode ser provada e verificada por máquina?
• Por que os assistentes de prova são confiáveis e qual é a base de computação confiável?
• Como a correspondência de Curry-Howard conecta provas e programas?
• O que é preciso para verificar sistemas reais como compiladores e kernels?

Key theories

Abordagem LCF para prova confiável

O Edinburgh LCF de Gordon, Milner e Wadsworth introduziu um pequeno kernel de prova confiável através do qual todos os teoremas devem passar, de modo que mesmo a automação complexa não pode produzir provas inconsistentes.

Compilador verificado (CompCert)

O CompCert de Leroy é um compilador C provado correto em um assistente de prova, com um teorema verificado por máquina de que o código gerado refina a semântica do programa fonte.

Kernel de sistema operacional verificado (seL4)

Klein e colegas produziram uma prova verificada por máquina de correção funcional para o microkernel seL4, demonstrando a verificação de ponta a ponta de software de sistemas de baixo nível.

Clinical relevance

A verificação mecanizada oferece a mais alta garantia disponível para software crítico, produzindo compiladores, kernels e bibliotecas criptográficas com garantias comprovadas, em vez de confiança baseada em testes. Assistentes de prova também são cada vez mais usados para formalizar a própria matemática.

History

A prova de teoremas interativa começou com o Edinburgh LCF na década de 1970, cuja metalinguagem ML e kernel confiável moldaram sistemas posteriores. Assistentes baseados em teoria de tipos, como Coq e Agda, e sistemas de lógica de ordem superior, como Isabelle/HOL, amadureceram nas décadas seguintes, culminando em artefatos verificados marcantes: o compilador CompCert (2009) e o kernel seL4 (2009).

Debates

Custo da verificação versus garantia obtida

A construção de provas verificadas por máquina de grandes sistemas exige um esforço enorme, o que gera debate sobre onde a verificação completa se justifica versus onde métodos mais leves são suficientes, e o quanto da prova pode ser automatizado.

Key figures

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

Seminal works

• gordon1979
• leroy2009
• klein2009
• harper2016

Frequently asked questions

O que é um assistente de prova?

Um assistente de prova é um software no qual um usuário constrói provas formais interativamente enquanto o sistema verifica mecanicamente cada etapa, de modo que uma prova concluída é confiável até um kernel pequeno e bem examinado.

Como a verificação de um programa difere de testá-lo?

Testar verifica o comportamento em entradas selecionadas e só pode revelar a presença de bugs, enquanto a verificação formal prova a correção para todas as entradas permitidas pela especificação, estabelecendo a ausência dos erros especificados.