BLAST (статический анализатор) (BLAST (vmgmncyvtnw gugln[gmkj))
| BLAST | |
|---|---|
| Тип | Инструменты статического анализа |
| Авторы | Dirk Beyer, Thomas Henzinger, Ranjit Jhala, Rupak Majumdar, Berkeley |
| Разработчики | Mikhail Mandrykin, Vadim Mutilin, Pavel Shved, ИСП РАН |
| Написана на | OCaml |
| Операционная система | Linux |
| Последняя версия | 2.7.3 (2014-11-18) |
| Лицензия | Apache License, Version 2.0 |
| Сайт | forge.ispras.ru/projects… |
Berkeley Lazy Abstraction Software Verification Tool (BLAST) — программа проверки моделей для языка Си. Задача, решаемая инструментом BLAST — это проверка того, что программа удовлетворяет поведенческим требованиям к ней. BLAST реализует подход абстракция и уточнение по контрпримерам (англ. counterexample-driven automatic abstraction refinement) для конструирования абстрактной модели, которая затем проверяется на свойства безопасности (англ. safety). Абстракция строится по ходу анализа и только до требуемой точности, устанавливаемой в ходе анализа.
Оригинальная версия BLAST[1], разработанная в Беркли, более не поддерживается. В настоящее время BLAST развивается и используется в ИСП РАН. Команда ИСП РАН регулярно участвует с инструментом BLAST в Международных соревнованиях по верификации программного обеспечения (SV-COMP).
В 2012 инструмент был награждён золотой медалью в категории DeviceDrivers64 на первых соревнованиях SV-COMP 2012, проводившихся на конференции TACAS 2012 в Таллине. [2]
В 2013 году - бронзовой в категории DeviceDrivers64 на вторых соревнованиях SV-COMP 2013, проводившихся на конференции TACAS 2013 в Риме. [3]
В 2014 году инструмент был награждён золотой медалью в категории DeviceDrivers64 на третьих соревнованиях SV-COMP 2014, проводившихся на конференции TACAS 2014 в Гренобле. [4]
Литература
[править | править код]- Pavel Shved, Mikhail Mandrykin, Vadim Mutilin. Predicate Analysis with BLAST 2.7. // Tools and Algorithms for the Construction and Analysis of Systems (англ.) / Flanagan, Cormac; König, Barbara. — Springer-Verlag, 2012. — Vol. 7214. — P. 525—527. — (Lecture Notes in Computer Science). — ISBN 978-3-642-28756-5.
- Beyer, Dirk; Henzinger, Thomas A.; Jhala, Ranjit; Majumdar, Rupak. The Software Model Checker Blast (неопр.) // International Journal on Software Tools for Technology Transfer. — 2007. — Т. 9, № 5—6. — С. 505—525. — doi:10.1007/s10009-007-0044-z.
- Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Gregoire Sutre. Software Verification with Blast // Proceedings of the 10th SPIN Workshop on Model Checking Software (SPIN 2003) (англ.) / Ball, Thomas; Rajamani, Sriram K.. — Springer-Verlag, 2003. — Vol. 2648. — P. 235—239. — (Lecture Notes in Computer Science). — ISBN 3-540-40117-2.
См. также
[править | править код]Примечания
[править | править код]- ↑ The Model Checker BLAST. Дата обращения: 16 ноября 2009. Архивировано 5 ноября 2009 года.
- ↑ Dirk Beyer (2012). "Competition on Software Verification (SV-COMP)" (PDF). Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and of Analysis Systems. Springer-Verlag, Heidelberg. Архивировано из оригинала (PDF) 4 марта 2016. Дата обращения: 24 декабря 2014.
- ↑ Dirk Beyer (2013). "Second Competition on Software Verification (Summary of SV-COMP 2013)" (PDF). Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and of Analysis Systems. Springer-Verlag, Heidelberg. Архивировано из оригинала (PDF) 24 сентября 2015. Дата обращения: 24 декабря 2014.
- ↑ Dirk Beyer (2014). "Third Competition on Software Verification (Summary of SV-COMP 2014)" (PDF). Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and of Analysis Systems. Springer-Verlag, Heidelberg. Архивировано из оригинала (PDF) 24 декабря 2014. Дата обращения: 24 декабря 2014.