La verificación formal o prueba formal es una prueba formal del cumplimiento o incumplimiento del sujeto de verificación con su descripción formal. El tema es algoritmos, programas y otras pruebas.
Debido a la naturaleza rutinaria de incluso la simple verificación formal y la posibilidad teórica de su completa automatización, la verificación formal generalmente significa verificación automática usando un programa .
Las pruebas de software no pueden probar que un sistema, algoritmo o programa no contenga errores ni defectos y satisfaga una determinada propiedad. Esto se puede hacer mediante verificación formal .
La verificación formal se puede utilizar para verificar sistemas como software de código fuente, protocolos criptográficos , circuitos lógicos combinatorios, circuitos digitales con memoria interna.
La verificación es una prueba formal sobre un modelo matemático abstracto del sistema, bajo el supuesto de que la correspondencia entre el modelo matemático y la naturaleza del sistema se considera inicialmente dada. Por ejemplo, para construir un modelo o análisis matemático y probar la corrección de algoritmos y programas.
Ejemplos de objetos matemáticos que se utilizan a menudo para el modelado y la verificación formal de programas y sistemas son:
Existen los siguientes enfoques para la verificación formal:
La programación basada en evidencia es una tecnología utilizada en círculos académicos en la década de 1980 para desarrollar programas para computadoras con pruebas de corrección - pruebas de la ausencia de errores en los programas (entendiendo, en el marco de esta teoría, los errores como discrepancias entre el algoritmo concebido y el algoritmo real implementado por el programa).
La demostración puede automatizarse completamente solo para un círculo muy pequeño de teorías simples, por lo que su verificación automática y, para ello, la transformación a una forma verificable se vuelve importante. Un número significativo de problemas prácticamente importantes, incluido, por ejemplo, el problema de parada , son algorítmicamente irresolubles .
Para mantener el rigor al verificar una prueba por un verificador, también se debe verificar el verificador, para lo cual se necesita un verificador más, y así sucesivamente. La cadena infinita resultante de verificadores podría colapsarse construyendo un verificador de autoverificación que tenga la capacidad de convertirse en uno práctico.