Hispanopedia Wiki
Articulo de referencia

CPAchecker

CPAchecker es un marco y una herramienta para la verificación formal de software [ 1 ] y el análisis de programas en C. Algunas de sus ideas y conceptos, como la abstracción per...

Hispanopedia WikiContenido en espanolLectura gratuita

CPAchecker es un marco y una herramienta para la verificación formal de software [ 1 ] y el análisis de programas en C. Algunas de sus ideas y conceptos, como la abstracción perezosa, se heredaron del verificador de modelos de software BLAST [ 2 ] . CPAchecker se basa en la idea del análisis de programas configurable [ 3 ] , un concepto que permite expresar tanto la verificación de modelos como el análisis de programas con un mismo formalismo. Al ejecutarse, CPAchecker realiza un análisis de alcanzabilidad , es decir, comprueba si un estado determinado, que viola una especificación dada, puede alcanzarse potencialmente [ 4 ] .

Una aplicación de CPAchecker es la verificación de controladores de dispositivos Linux . [ 5 ]

Logros

CPAchecker obtuvo el primer lugar en dos categorías (General y ControlFlowInteger) en la 1.ª Competencia de Verificación de Software (2012) que se llevó a cabo en TACAS 2012 en Tallin . [ 6 ]

CPAchecker obtuvo el primer lugar (categoría General) en la 2.ª Competencia de Verificación de Software (2013) que se llevó a cabo en TACAS 2013 en Roma . [ 7 ]

Arquitectura

CPAchecker funciona con un autómata de flujo de control (CFA); antes de que un programa en C pueda ser analizado por el algoritmo CPA, se transforma en un CFA. Un CFA es un grafo dirigido cuyas aristas representan supuestos o asignaciones, y cuyos nodos representan ubicaciones del programa.

Referencias

  1. ↑ Sitio web oficial de CPAchecker: https://cpachecker.sosy-lab.org
  2. ↑ Dirk Beyer y Thomas A. Henzinger y Ranjit Jhala y Rupak Majumdar (2007). "El verificador de modelos de software BLAST: aplicaciones a la ingeniería de software" (PDF) . Revista internacional sobre herramientas de software para la transferencia de tecnología . 9 : 505–525 . doi : 10.1007/s10009-007-0044-z . S2CID 1662778 . 
  3. ↑ Dirk Beyer, Thomas A. Henzinger y Grégory Théoduloz (2007). «Verificación de software configurable: Concretizando la convergencia de la verificación de modelos y el análisis de programas» (PDF) . Actas de la 19.ª Conferencia Internacional sobre Verificación Asistida por Computadora . Springer-Verlag, Heidelberg. ISBN 978-3-540-73367-6.
  4. ↑ Dirk Beyer y M. Erkan Keremoglu (2011). «CPAchecker: Una herramienta para la verificación de software configurable» (PDF) . Actas de la 23.ª Conferencia Internacional sobre Verificación Asistida por Computadora . Springer-Verlag, Heidelberg. ISBN 978-3-642-22109-5.
  5. ↑ Verificación de controladores Linux: http://linuxtesting.org/project/ldv
  6. ↑ Dirk Beyer (2012). "Competencia sobre verificación de software (SV-COMP)" (PDF) . Actas de la 18.ª Conferencia Internacional sobre Herramientas y Algoritmos para la Construcción y Análisis de Sistemas . Springer-Verlag, Heidelberg.
  7. ↑ Dirk Beyer (2013). "Segunda competición sobre verificación de software (Resumen de SV-COMP 2013)" (PDF) . Actas de la 19.ª Conferencia Internacional sobre Herramientas y Algoritmos para la Construcción y el Análisis de Sistemas . Springer-Verlag, Heidelberg.
  • Sitio web oficial