CPAchecker
CPAchecker — это платформа и инструмент для формальной проверки программного обеспечения . [1] и анализ программ программ C- . Некоторые его идеи и концепции, например ленивая абстракция, были унаследованы от программного средства проверки моделей BLAST . [2] CPAchecker основан на идее настраиваемого программного анализа. [3] это концепция, которая позволяет выразить как проверку модели , так и анализ программы с помощью одного формализма.При запуске CPAchecker выполняет анализ достижимости , т. е. проверяет, может ли потенциально быть достигнуто определенное состояние, которое нарушает заданную спецификацию. [4]
Одним из применений CPAchecker является проверка Linux драйверов устройств . [5]
Достижения
[ редактировать ]CPAchecker занял первое место в двух категориях (Overall и ControlFlowInteger) на 1-м конкурсе по верификации программного обеспечения (2012 г.), который проходил на выставке TACAS 2012 в Таллинне . [6]
CPAchecker занял первое место (в общей категории) на 2-м конкурсе по проверке программного обеспечения (2013 г.), который проходил на выставке TACAS 2013 в Риме . [7]
Архитектура
[ редактировать ]CPAchecker работает на автомате потока управления (CFA); Прежде чем данная программа C может быть проанализирована алгоритмом CPA, она преобразуется в CFA. CFA — это ориентированный граф, ребра которого представляют либо предположения, либо назначения, а его узлы представляют местоположения программ.
Ссылки
[ редактировать ]- ^ Официальный сайт CPAchecker: http://cpachecker.sosy-lab.org.
- ^ Дирк Бейер, Томас А. Хензингер, Ранджит Джала и Рупак Маджумдар (2007). «Проверка моделей программного обеспечения BLAST: приложения для разработки программного обеспечения» (PDF) . Международный журнал по программным инструментам для трансфера технологий . 9 : 505–525. дои : 10.1007/s10009-007-0044-z . S2CID 1662778 .
- ^ Дирк Бейер, Томас А. Хенцингер и Грегори Теодулоз (2007). «Верификация настраиваемого программного обеспечения: конкретизация сходимости проверки модели и анализа программы» (PDF) . Материалы 19-й Международной конференции по компьютерному контролю . Шпрингер-Верлаг, Гейдельберг. ISBN 978-3-540-73367-6 .
- ^ Дирк Бейер и М. Эркан Керемоглу (2011). «CPAchecker: инструмент для настраиваемой проверки программного обеспечения» (PDF) . Материалы 23-й Международной конференции по компьютерному контролю . Шпрингер-Верлаг, Гейдельберг. ISBN 978-3-642-22109-5 .
- ^ Проверка драйвера Linux: http://linuxtesting.org/project/ldv.
- ^ Дирк Бейер (2012). «Конкурс по верификации программного обеспечения (СВ-КОМП)» (PDF) . Материалы 18-й Международной конференции по средствам и алгоритмам построения и анализа систем . Шпрингер-Верлаг, Гейдельберг.
- ^ Дирк Бейер (2013). «Второй конкурс по верификации программного обеспечения (Итоги SV-COMP 2013)» (PDF) . Материалы 19-й Международной конференции по инструментам и алгоритмам построения и анализа систем . Шпрингер-Верлаг, Гейдельберг.