Verificação formal – Wikipédia, a enciclopédia livre

Verificação formal é a prova matemática da conformidade de um algoritmo a certa especificação formal ou propriedade, usando métodos formais.

A verificação formal pode ser usada em sistemas como protocolos de criptografia, circuitos combinatórios, circuitos digitais com memória interna e programas de computador expressados através de código fonte. A verificação desses sistemas é feita fornecendo uma prova matemática num modelo matemático abstrato do sistema, a correspondência entre o modelo matemático e toda a natureza do sistema conhecido por construção. Exemplos de estruturas usadas para modelar sistemas incluem máquinas de estado finito, redes de Petri, além de semânticas formais como operacional, denotacional, axiomática e a lógica de Hoare.

Atualmente existem basicamente duas abordagens para a verificação formal.

A primeira é a verificação de modelos, que consiste numa exploração sistematicamente exaustiva do modelo matemático, o que é possível para modelos finitos, mas também para modelos infinitos em que conjuntos finitos de estados podem ser representados. Isso geralmente consiste na exploração de todos os estados e transições do modelo, ao usar técnicas de abstração para considerar grupos de estados numa única operação, reduzindo o tempo de processamento.

A segunda abordagem é a inferência lógica, que consiste na utilização duma formalização matemática do sistema, através do uso de software de prova de teoremas. Esse processo é geralmente automatizado parcialmente, dependendo do entendimento manual do sistema para a validação.

• Prova automática de teoremas