WikiDer > CPAchecker

CPAchecker

CPAchecker это фреймворк и инструмент для формальная проверка программного обеспечения,[1] и программный анализ, из C программы. Некоторые из его идей и концепций, например ленивая абстракция, были унаследованы от программа проверки моделей BLAST.[2]CPAchecker основан на идее конфигурируемого программного анализа.[3]это концепция, позволяющая выразить как проверка модели и программный анализ с одним формализмом. При выполнении CPAchecker выполняет достижимость анализ, то есть он проверяет, может ли потенциально быть достигнуто определенное состояние, которое нарушает заданную спецификацию.[4]

Одно из применений CPAchecker - это проверка Linux драйверы устройств.[5]

Достижения

CPAchecker занял первое место в двух категориях (Общие и ControlFlowInteger) в 1-м конкурсе по верификации программного обеспечения (2012 г.), который проводился на TACAS 2012 г. Таллинн.[6]

CPAchecker занял первое место (категория в целом) во 2-м конкурсе по верификации программного обеспечения (2013 г.), который проводился на TACAS 2013 г. Рим.[7]

Архитектура

CPAchecker работает на автоматы потока управления (CFA); прежде чем данная программа на C может быть проанализирована алгоритмом CPA, она преобразуется в CFA. CFA - это ориентированный граф, ребра которого представляют либо предположения, либо назначения, а его узлы представляют собой местоположения программ.

Рекомендации

  1. ^ Официальный сайт CPAchecker: http://cpachecker.sosy-lab.org
  2. ^ Дирк Бейер и Томас А. Хензингер, Ранджит Джала и Рупак Маджумдар (2007). "Средство проверки модели программного обеспечения BLAST: приложения для разработки программного обеспечения" (PDF). Международный журнал программных средств для передачи технологий (STTT). 9: 505–525. Дои:10.1007 / s10009-007-0044-z.
  3. ^ Дирк Бейер, Томас А. Хензингер и Грегори Теодуло (2007). «Конфигурируемая проверка программного обеспечения: конкретизация конвергенции проверки модели и программного анализа» (PDF). Материалы 19-й Международной конференции по компьютерной верификации. Springer-Verlag, Гейдельберг. ISBN 978-3-540-73367-6.
  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, Гейдельберг.

внешняя ссылка