CPAchecker

Инструмент тестирования программного обеспечения, написанный на Java

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. doi :10.1007/s10009-007-0044-z. S2CID 1662778.
^ Дирк Бейер и Томас А. Хензингер и Грегори Теодуло (2007). "Конфигурируемая проверка программного обеспечения: конкретизация сходимости проверки моделей и анализа программ" (PDF) . Труды 19-й Международной конференции по компьютерной верификации . Springer-Verlag, Гейдельберг. ISBN 978-3-540-73367-6.
^ Дирк Бейер и М. Эркан Керемоглу (2011). "CPAchecker: инструмент для настраиваемой проверки программного обеспечения" (PDF) . Труды 23-й Международной конференции по компьютерной проверке . Springer-Verlag, Гейдельберг. ISBN 978-3-642-22109-5.
^ Проверка драйвера Linux: http://linuxtesting.org/project/ldv
^ Дирк Бейер (2012). "Конкурс по верификации программного обеспечения (SV-COMP)" (PDF) . Труды 18-й Международной конференции по инструментам и алгоритмам для построения и анализа систем . Springer-Verlag, Гейдельберг.
^ Дирк Бейер (2013). "Второй конкурс по верификации программного обеспечения (резюме SV-COMP 2013)" (PDF) . Труды 19-й Международной конференции по инструментам и алгоритмам для построения и анализа систем . Springer-Verlag, Гейдельберг.

Внешние ссылки

Официальный сайт

[1] Официальный сайт CPAchecker: http://cpachecker.sosy-lab.org

[Blast-2] Дирк Бейер и Томас А. Хензингер и Ранджит Джала и Рупак Маджумдар (2007). "Проверка моделей программного обеспечения BLAST: применение в программной инженерии" (PDF) . Международный журнал по программным инструментам для передачи технологий . 9 : 505–525. doi :10.1007/s10009-007-0044-z. S2CID 1662778.

[3] Дирк Бейер и Томас А. Хензингер и Грегори Теодуло (2007). "Конфигурируемая проверка программного обеспечения: конкретизация сходимости проверки моделей и анализа программ" (PDF) . Труды 19-й Международной конференции по компьютерной верификации . Springer-Verlag, Гейдельберг. ISBN 978-3-540-73367-6.

[cpachecker-4] Дирк Бейер и М. Эркан Керемоглу (2011). "CPAchecker: инструмент для настраиваемой проверки программного обеспечения" (PDF) . Труды 23-й Международной конференции по компьютерной проверке . Springer-Verlag, Гейдельберг. ISBN 978-3-642-22109-5.

[5] Проверка драйвера Linux: http://linuxtesting.org/project/ldv

[6] Дирк Бейер (2012). "Конкурс по верификации программного обеспечения (SV-COMP)" (PDF) . Труды 18-й Международной конференции по инструментам и алгоритмам для построения и анализа систем . Springer-Verlag, Гейдельберг.

[7] Дирк Бейер (2013). "Второй конкурс по верификации программного обеспечения (резюме SV-COMP 2013)" (PDF) . Труды 19-й Международной конференции по инструментам и алгоритмам для построения и анализа систем . Springer-Verlag, Гейдельберг.