Verificación formal

La verificación formal, en ingeniería y en computación, 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.

Importancia en las matemáticas

Tradicionalmente, dentro de las matemáticas, la verificación únicamente se utilizaba para la demostración y convicción de enunciados matemáticos y como medio de obtención de evidencias para la eliminación de dudas. Pero en la realidad tiene un mayor número de funciones, a parte de la de convicción:

  • En su uso típico de convicción, como se ha dicho anteriormente, se basa en la demostración de enunciados y de conjeturas desconocidas, verificación deductiva. En este estudio, los matemáticos, además de partir de las premisas, construyen contraejemplos mediante una serie de pruebas, llamadas pruebas cuasi-empíricas, las cuales, intentan descubrir contradicciones o errores ocultos.
Uno de los métodos de esta verificación, es la llamada demostración deductiva, en donde la conclusión proviene de las premisas. Un defecto de esta demostración, es que se da lugar unos desarrollos tan extensos y complicados que el riesgo de cometer errores aumenta.
  • Como método de sistematización. Aquí, la verificación no comprueba si algunas afirmaciones son ciertas o no, sino que se encarga de organizar enunciados individuales no relacionados. De esta manera, ayuda a identificar inconsistencias, a simplificar las teorías matemáticas (integrando afirmaciones y teoremas), a economizar los resultados, a ayudar a las aplicaciones mediante el análisis de sus axiomas y definiciones, etc.
  • Como método de explicación. Aunque es posible alcanzar la afirmación mediante la verificación deductiva, en la mayoría de los casos, esta no proporciona una explicación válida de por qué puede ser verdadero y únicamente confirma que es verdad. Así, en los casos en los que los resultados están defendidos por evidencias cuasi-empíricas concluyentes, la función de la verificación no es únicamente la de convencer, sino también la de explicar. Más aún, para los matemáticos es más primordial este aspecto aclaratorio, que el simple hecho de verificación.
  • Como verificación de modelos. Este tipo de verificación, consiste en un reconocimiento del modelo matemático (aplicable tanto para modelos finitos, como para modelos infinitos, ya que estos últimos se pueden representar de manera finita mediante la abstracción).
En definitiva, consiste en estudiar todos los cambios y estados de los modelos matemáticos mediante técnicas inteligentes de abstracción, consiguiendo agrupar en una sola operación todo el conjunto de estados. Estas transiciones estudiadas, son descritas en diferentes lógicas, tales como, la lógica computacional, la lógica temporal ...[2]