Verificación formal

Introducción

Generalmente, a la verificación, se la define como la comprobación o control de alguna cosa u objeto.

Más específicamente, sobre todo en ingeniería y en la computación, esta revisión es conocida como verificación formal.
La verificación formal, dentro de estas ciencias, 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 lenguaje lógico (como la lógica de primer orden), se puede encontrar una demostración o prueba de corrección de un programa, algoritmo, etc, aunque también se puede encontrar su refutación.[1] Es un método necesario para probar cualquier programa o teoría pero, aunque sea satisfactoria, no asegura que la solución sea del todo correcta.

Dentro de la computación, la verificación es usada para estudiar los distintos sistemas software (en código fuente), sistemas combinacionales, circuitos digitales, etc.

Uno de los precursores de la verificación fue Edsger Dijkstra que, mostrando mucho interés en ella durante los 70, publicó el libro "A Discipline of Programming", en el cual, presentó su método de desarrollo sistemático de programas junto con sus pruebas de corrección, todos ellos basados en la verificación formal.

Other Languages