Verificación formal

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


Wikimedia foundation. 2010.

Игры ⚽ Нужно сделать НИР?

Mira otros diccionarios:

  • Verificación formal — Mediante el uso de la lógica de primer orden y unas reglas, la verificación formal consiste en demostrar que un algoritmo determinado cumple una postcondición (que no es más que una fórmula de lógica de predicados) suponiendo que se cumple una… …   Enciclopedia Universal

  • Método formal — En ingeniería de software un método formal es un camino a la construcción y análisis de modelos matemáticos que permitan una automatización del desarrollo de sistemas informáticos. Los métodos formales se caracterizan por emplear técnicas y… …   Wikipedia Español

  • ACL2 — es, a la vez, un lenguaje de programación, una lógica matemática para especificar y demostrar formalmente propiedades de los programas escritos en dicho lenguaje, y un demostrador automático de teoremas que asiste al usuario en dicha tarea. ACL2… …   Wikipedia Español

  • Teoría de la computación — La teoría de la computación es una rama de la matemática y la computación que centra su interés en las limitaciones y capacidades fundamentales de las computadoras. Específicamente esta teoría busca modelos matemáticos que formalizan el concepto… …   Wikipedia Español

  • Lógica de Hoare — Este artículo o sección necesita referencias que aparezcan en una publicación acreditada, como revistas especializadas, monografías, prensa diaria o páginas de Internet fidedignas. Puedes añadirlas así o avisar …   Wikipedia Español

  • Edsger Dijkstra — Saltar a navegación, búsqueda Edsger Wybe Dijkstra …   Wikipedia Español

  • SPARK — Saltar a navegación, búsqueda Para otros usos de este término, véase Spark (desambiguación). SPARK es un lenguaje de programación especialmente diseñado para sistemas de alta integridad. Es un subconjunto anotado de Ada desarrollado por la… …   Wikipedia Español

  • Convención sobre armas biológicas — Esta página o sección está siendo traducida del idioma inglés a partir del artículo Biological Weapons Convention, razón por la cual puede haber lagunas de contenidos, errores sintácticos o escritos sin traducir. Puedes colaborar con… …   Wikipedia Español

  • Matemáticas discretas — Las matemáticas discretas son un área de las matemáticas encargadas del estudio de los conjuntos discretos: finitos o infinitos numerables. En oposición a las matemáticas continuas, que se encarga del estudio de conceptos como la continuidad y el …   Wikipedia Español

  • Spin — El término spin hace referencia a varios artículos: Contenido 1 Aeronáutica 2 Física 3 Botánica 4 Geografía …   Wikipedia Español

Compartir el artículo y extractos

Link directo
Do a right-click on the link above
and select “Copy Link”