Hispanopedia Wiki
Articulo de referencia

Comprobador de modelos BLAST

{{Cite web | url=http://forge.ispras.ru/projects/blast/files |title = Files - BLAST - Open-Source Projects}} "},"latest release date":{"wt":"{{Start date and age|df=yes|2015|10|...

Hispanopedia WikiContenido en espanolLectura gratuita

La herramienta de verificación de software de abstracción perezosa de Berkeley ( BLAST ) es una herramienta de verificación de modelos de software para programas en C. La tarea que aborda BLAST es la necesidad de verificar si el software satisface los requisitos de comportamiento de sus interfaces asociadas. BLAST emplea un refinamiento automático de abstracción basado en contraejemplos para construir un modelo abstracto que luego se verifica para comprobar sus propiedades de seguridad. La abstracción se construye sobre la marcha y solo con la precisión requerida .

Logros

BLAST quedó primero en la categoría DeviceDrivers64 en la 1.ª Competición de Verificación de Software (2012) que se celebró en TACAS 2012 en Tallin . [ 2 ]

BLAST quedó tercero (categoría DeviceDrivers64) en la 2ª Competición de Verificación de Software (2013) que se celebró en TACAS 2013 en Roma . [ 3 ]

BLAST quedó primero en la categoría DeviceDrivers64 en la 3ª Competición de Verificación de Software (2014), que se celebró en TACAS 2014 en Grenoble . [ 4 ]

Referencias

  1. ↑ "Archivos - BLAST - Proyectos de código abierto" .
  2. ↑ 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.
  3. ↑ 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.
  4. ↑ Dirk Beyer (2014). "Tercera competición sobre verificación de software (Resumen de SV-COMP 2014)" (PDF) . Actas de la 20.ª Conferencia Internacional sobre Herramientas y Algoritmos para la Construcción y el Análisis de Sistemas . Springer-Verlag, Heidelberg.
Notas
  • Pavel Shved; Mikhail Mandrykin; Vadim Mutilin (2012). "Análisis de predicados con BLAST 2.7". En Flanagan, Cormac; König, Barbara (eds.). Herramientas y algoritmos para la construcción y el análisis de sistemas . Lecture Notes in Computer Science. Vol.  7214. Springer-Verlag. pp. 525–527 . ISBN  978-3-642-28756-5.
  • Beyer, Dirk; Henzinger, Thomas A.; Jhala, Ranjit; Majumdar, Rupak (2007). "The Software Model Checker Blast". International Journal on Software Tools for Technology Transfer . 9 ( 5– 6): 505– 525. doi : 10.1007/s10009-007-0044-z . S2CID 1662778 . 
  • Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar y Gregoire Sutre (2003). «Verificación de software con Blast». En Ball, Thomas y Rajamani, Sriram K. (eds.). Actas del 10.º Taller SPIN sobre Verificación de Modelos de Software (SPIN 2003) . Lecture Notes in Computer Science. Vol.  2648. Springer-Verlag. pp. 235–239 . ISBN  3-540-40117-2.
  • Sitio web de BLAST 2.5
  • Sitio web de BLAST 2.7