WikiSort.ru - Не сортированное

ПОИСК ПО САЙТУ | о проекте
BLAST
Тип Инструменты статического анализа
Автор Dirk Beyer, Thomas Henzinger, Ranjit Jhala, Rupak Majumdar, Berkeley
Разработчик Mikhail Mandrykin, Vadim Mutilin, Pavel Shved, ИСП РАН
Операционная система Linux
Последняя версия 2.7.3 (18.11.2014)
Лицензия 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. — Springer-Verlag, 2012. — Vol. 7214. — P. 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.
  • 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). — Springer-Verlag, 2003. — Vol. 2648. — P. 235–239. — ISBN 3-540-40117-2.

См. также

Примечания

  1. ↑ The Model Checker BLAST
  2. ↑ Dirk Beyer (2012). "Competition on Software Verification (SV-COMP)". Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and of Analysis Systems, Springer-Verlag, Heidelberg. 
  3. ↑ Dirk Beyer (2013). "Second Competition on Software Verification (Summary of SV-COMP 2013)". Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and of Analysis Systems, Springer-Verlag, Heidelberg. 
  4. ↑ Dirk Beyer (2014). "Third Competition on Software Verification (Summary of SV-COMP 2014)". Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and of Analysis Systems, Springer-Verlag, Heidelberg. 

Ссылки

Данная страница на сайте WikiSort.ru содержит текст со страницы сайта "Википедия".

Если Вы хотите её отредактировать, то можете сделать это на странице редактирования в Википедии.

Если сделанные Вами правки не будут кем-нибудь удалены, то через несколько дней они появятся на сайте WikiSort.ru .



Текст в блоке "Читать" взят с сайта "Википедия" и доступен по лицензии Creative Commons Attribution-ShareAlike; в отдельных случаях могут действовать дополнительные условия.

Другой контент может иметь иную лицензию. Перед использованием материалов сайта WikiSort.ru внимательно изучите правила лицензирования конкретных элементов наполнения сайта.

2019-2024
WikiSort.ru - проект по пересортировке и дополнению контента Википедии