- Verificación formal
-
La verificación formal es un método de validación estática (se valida a través del propio código del programa, a partir de una abstracción o de una representación simbólica), en el que partiendo de un conjunto axiomático, reglas de inferencia y algún lenguage lógico (como la lógica de primer orden u otra de preferencia una lógica sólida y completa), se puede encontrar una demostración o prueba de corrección de un programa.
Véase también
- Lógica de Hoare, un sistema formal que permite la verificación de programas imperativos.
Wikimedia foundation. 2010.