Verificación Formal y Asistentes de Pruebas
La verificación formal establece, mediante pruebas matemáticas verificadas por máquina, que el software cumple con su especificación; los asistentes de pruebas son las herramientas que construyen y verifican dichas pruebas.
Definition
La verificación formal es la construcción de una prueba rigurosa y verificada por máquina de que un sistema satisface una especificación formal, y un asistente de pruebas es un software que ayuda a un usuario a desarrollar dichas pruebas y verifica mecánicamente su validez.
Scope
Este tema abarca la verificación deductiva y la demostración interactiva de teoremas: asistentes de pruebas basados en la teoría de tipos o lógica de orden superior (como Coq, Isabelle, Lean y Agda), el enfoque LCF para pruebas confiables, el fundamento de proposiciones-como-tipos, la automatización de pruebas y tácticas, y artefactos verificados emblemáticos que incluyen compiladores y núcleos de sistemas operativos.
Core questions
- ¿Cómo se puede probar y verificar por máquina la corrección funcional completa?
- ¿Por qué son confiables los asistentes de pruebas y cuál es la base de computación confiable?
- ¿Cómo conecta la correspondencia de Curry-Howard las pruebas y los programas?
- ¿Qué se necesita para verificar sistemas reales como compiladores y núcleos?
Key theories
- Enfoque LCF para pruebas confiables
- El Edinburgh LCF de Gordon, Milner y Wadsworth introdujo un pequeño núcleo de prueba confiable a través del cual deben pasar todos los teoremas, de modo que incluso la automatización compleja no pueda producir pruebas erróneas.
- Compilador verificado (CompCert)
- CompCert de Leroy es un compilador C cuya corrección ha sido probada en un asistente de pruebas, con un teorema verificado por máquina que establece que el código generado refina la semántica del programa fuente.
- Núcleo de sistema operativo verificado (seL4)
- Klein y sus colegas produjeron una prueba verificada por máquina de la corrección funcional para el micronúcleo seL4, demostrando la verificación de extremo a extremo de software de sistemas de bajo nivel.
Clinical relevance
La verificación mecanizada ofrece la mayor garantía disponible para software crítico, produciendo compiladores, núcleos y bibliotecas criptográficas con garantías probadas en lugar de la confianza basada en pruebas. Los asistentes de pruebas también se utilizan cada vez más para formalizar las propias matemáticas.
History
La demostración interactiva de teoremas comenzó con Edinburgh LCF en la década de 1970, cuyo metalenguaje ML y núcleo de confianza moldearon sistemas posteriores. Asistentes basados en la teoría de tipos como Coq y Agda, y sistemas de lógica de orden superior como Isabelle/HOL, maduraron durante las décadas siguientes, culminando en artefactos verificados emblemáticos: el compilador CompCert (2009) y el núcleo seL4 (2009).
Debates
- Costo de la verificación versus la garantía obtenida
- La construcción de pruebas verificadas por máquina de sistemas grandes requiere un esfuerzo enorme, lo que provoca un debate sobre dónde se justifica la verificación completa frente a dónde son suficientes los métodos más ligeros, y cuánto se puede automatizar la prueba.
Key figures
- Robin Milner
- Michael Gordon
- Xavier Leroy
- Gerwin Klein
- Robert Harper
Related topics
Seminal works
- gordon1979
- leroy2009
- klein2009
- harper2016
Frequently asked questions
- ¿Qué es un asistente de pruebas?
- Un asistente de pruebas es un software en el que un usuario construye pruebas formales de forma interactiva mientras el sistema verifica mecánicamente cada paso, de modo que una prueba completada es confiable hasta un núcleo pequeño y bien examinado.
- ¿En qué se diferencia la verificación de un programa de su prueba (testing)?
- Las pruebas (testing) verifican el comportamiento en entradas seleccionadas y solo pueden revelar la presencia de errores, mientras que la verificación formal prueba la corrección para todas las entradas permitidas por la especificación, estableciendo la ausencia de los errores especificados.