La herramienta de Berkeley Lazy abstracción de software de verificación ( BLAST ) es un software de control de modelo de herramienta para los programas C . La tarea abordada por BLAST es la necesidad de verificar si el software satisface los requisitos de comportamiento de sus interfaces asociadas. BLAST emplea un refinamiento de abstracción automático impulsado por contraejemplos para construir un modelo abstracto que luego se verifica en el modelo para determinar las propiedades de seguridad. La abstracción se construye sobre la marcha y solo con la precisión solicitada .
Autor (es) original (es) | Dirk Beyer, Thomas Henzinger, Ranjit Jhala, Rupak Majumdar, Berkeley |
---|---|
Desarrollador (es) | Mikhail Mandrykin, Vadim Mutilin, Pavel Shved, Instituto de Programación de Sistemas |
Lanzamiento estable | 2.7.3 [1] / 30 de octubre de 2015 |
Escrito en | OCaml |
Sistema operativo | Linux |
Tipo | Análisis de código estático |
Licencia | Licencia Apache, versión 2.0 |
Sitio web | forjar |
Logros
BLAST ocupó el primer lugar en la categoría DeviceDrivers64 en el 1er Concurso de Verificación de Software (2012) que se celebró en TACAS 2012 en Tallin . [2]
BLAST ocupó el tercer lugar (categoría DeviceDrivers64) en el 2º Concurso de Verificación de Software (2013) que se celebró en TACAS 2013 en Roma . [3]
BLAST ocupó el primer lugar en la categoría DeviceDrivers64 en el 3er Concurso de Verificación de Software (2014) que se celebró en TACAS 2014 en Grenoble . [4]
Referencias
- ^ "Archivos - BLAST - Proyectos de código abierto" .
- ^ Dirk Beyer (2012). "Concurso de Verificación de Software (SV-COMP)" (PDF) . Actas de la XVIII Conferencia Internacional sobre Herramientas y Algoritmos para la Construcción y de Sistemas de Análisis . Springer-Verlag, Heidelberg.
- ^ Dirk Beyer (2013). "Segundo Concurso de Verificación de Software (Resumen de SV-COMP 2013)" (PDF) . Actas de la XIX Conferencia Internacional sobre Herramientas y Algoritmos para la Construcción y de Sistemas de Análisis . Springer-Verlag, Heidelberg.
- ^ Dirk Beyer (2014). "Tercer Concurso de Verificación de Software (Resumen de SV-COMP 2014)" (PDF) . Actas de la XX Conferencia Internacional sobre Herramientas y Algoritmos para la Construcción y de Sistemas de Análisis . 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 análisis de sistemas . Apuntes de conferencias en Ciencias de la Computación. 7214 . Springer-Verlag. págs. 525–527. ISBN 978-3-642-28756-5.
- Beyer, Dirk; Henzinger, Thomas A .; Jhala, Ranjit; Majumdar, Rupak (2007). "El software Model Checker Blast". Revista internacional de herramientas de software para la transferencia de tecnología . 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 décimo taller SPIN sobre software de verificación de modelos (SPIN 2003) . Apuntes de conferencias en Ciencias de la Computación. 2648 . Springer-Verlag. págs. 235-239. ISBN 3-540-40117-2.