Análisis y Verificación de Programas
El análisis y la verificación de programas utilizan técnicas rigurosas para razonar sobre lo que hacen los programas, detectando errores o demostrando que el software cumple con su especificación.
Definition
El análisis de programas es la derivación automatizada de propiedades del comportamiento de un programa sin ejecutarlo en todas las entradas, y la verificación de programas es el establecimiento, mediante prueba o verificación exhaustiva, de que un programa satisface una especificación formal.
Scope
Esta área abarca el razonamiento automatizado y semiautomatizado sobre programas: análisis estático y técnicas de flujo de datos, interpretación abstracta como un marco unificador para la aproximación sólida, verificación de modelos de sistemas de estado finito y concurrentes, y verificación deductiva con asistentes de prueba. Aborda la solidez, la compensación entre precisión y decidibilidad, y el uso de estos métodos para construir software confiable.
Sub-topics
Core questions
- ¿Cómo se pueden calcular las propiedades del programa de forma sólida a pesar de la indecidibilidad?
- ¿Cómo equilibran los análisis la precisión con la escalabilidad?
- ¿Cuándo se puede verificar la corrección de un sistema de forma exhaustiva en lugar de probarla?
- ¿Cómo se construyen y verifican por máquina las pruebas de corrección funcional completa?
Key theories
- Interpretación abstracta
- Cousot y Cousot establecieron un marco teórico de retículos en el que los análisis estáticos sólidos se derivan como aproximaciones de la semántica de un programa, unificando muchos análisis y garantizando su solidez.
- Verificación de modelos de lógica temporal
- Clarke, Emerson y Sistla demostraron cómo verificar automáticamente sistemas concurrentes de estado finito contra especificaciones de lógica temporal explorando exhaustivamente el espacio de estados.
- Verificación mecanizada de extremo a extremo
- El compilador verificado de Leroy demuestra que el software realista puede probarse como correcto con un asistente de prueba, lo que conlleva una garantía verificada por máquina de que la compilación preserva el comportamiento del programa.
Clinical relevance
El análisis y la verificación de programas sustentan herramientas que encuentran errores y vulnerabilidades de seguridad a gran escala, certifican software de aviónica y automotriz crítico para la seguridad, y producen compiladores y núcleos de sistemas operativos verificados por máquina. Convierten la corrección de una confianza basada en pruebas en garantías demostrables.
History
El análisis de flujo de datos surgió con los compiladores optimizadores en la década de 1970, la misma década en que los Cousot introdujeron la interpretación abstracta. La verificación de modelos surgió a principios de la década de 1980 a través de Clarke y Emerson e independientemente Queille y Sifakis, ganando más tarde un Premio Turing. La década de 2000 vio éxitos a gran escala en el análisis estático industrial y la verificación mecanizada, como CompCert y seL4.
Debates
- Solidez versus practicidad de los análisis
- Los desarrolladores de herramientas debaten si los análisis deben ser completamente sólidos, informando todos los posibles errores pero arriesgándose a muchas falsas alarmas, o deliberadamente no sólidos para reducir el ruido y la escala, una tensión que da forma a las herramientas industriales de detección de errores.
Key figures
- Patrick Cousot
- Radhia Cousot
- Edmund Clarke
- E. Allen Emerson
- Xavier Leroy
Related topics
Seminal works
- cousot1977
- clarke1986
- leroy2009
- nielson1999
Frequently asked questions
- ¿Cuál es la diferencia entre análisis estático y verificación?
- El análisis estático infiere automáticamente propiedades aproximadas (como posibles desreferencias nulas) sin especificaciones completas, mientras que la verificación demuestra que un programa satisface una especificación formal precisa, lo que generalmente requiere más esfuerzo y produce garantías más sólidas.
- Si la corrección es indecidible, ¿cómo puede funcionar el análisis?
- Los análisis eluden la indecidibilidad calculando aproximaciones sólidas: pueden informar algunas posibilidades que en realidad no pueden ocurrir, pero nunca omiten una violación real de la propiedad que verifican.