06.04.2019: CPAchecker-BAM-BnB и CPALockator на SV-COMP'2019

На международных соревнованиях инструментов статической верификации (SV-COMP 2019), проходивших в рамках международной конференции TACAS, Прага, Чехия, были представлены доклады по инструментам CPAchecker-BAM-BnB и CPALockator. В этом году наш инструмент CPAchecker-BAM-BnB завоевал золотую медаль в категории Software Systems, а CPALockator участвовал в категории Concurrency Safety.

Полные результаты соревнований SV-COMP 2019 доступны здесь: https://sv-comp.sosy-lab.org/2019/results/results-verified. В таблицах представлены победители в различных категориях.

Инструмент CPAchecker-BAM-BnB основывается на совместной работе с командой инструмента CPAchecker. Аббревиатура BAM обозначает запоминание абстракции блоков (англ. Block Abstraction Memoization), что позволяет переиспользовать результаты верификации во время анализа. BnB - это модификация модели памяти в предикатном анализе (см. статью).

Инструмент CPALockator реализует подход с раздельным анализом потоков (thread-modular approach) для верификации многопоточного программного обеспечения (см. плакат). Абстракция от взамодействия потоков позволяет увеличить скорость анализа. Однако, при этом уменьшается точность анализа, что может привести к ложным предупреждениям об ошибке. В отличие от других инструментов проверки моделей CPALockator успешно решает объемные примеры, основанные на драйверах ОС Linux. Некоторые из этих задач решаются только инструментом CPALockator. Однако, представленная реализация имеет технические ограничения, например, пока поддерживает только примитивы синхронизации на основе блокировок, поэтому теряет очки на рукописных примерах, реализующих алгоритмы синхронизации без блокировок. Тем не менее, CPALockator не выдает некорректных доказательств корректности программы (не пропускает ошибок), что подтверждает корректность подхода.

Мы благодарим сообщество CPAchecker за вклад в развитие платформы, на которой мы основываемся.