Верификация C-программ в мультиязыковой системе СПЕКТР

Представлена расширяемая мультиязыковая система анализа и верификации СПЕКТР, разрабатываемая в рамках одноименного проекта, и показаны перспективы ее использования на примере верификации C-программ. Проект СПЕКТР направлен на создание нового интегрированного подхода к верификации императивных программ, который позволяет интегрировать, унифицировать и комбинировать методы и техники верификации императивных программ, накапливать и использовать знания о них. Особенностью подхода является использование специализированного языка выполнимых спецификаций Atoment для разработки средств верификации программ, который позволяет представить в едином унифицированном формате как методы и техники верификации, так и данные для них (программные модели, аннотации, логические формулы). C-компонента системы СПЕКТР использует двухуровневый метод верификации C-программ. Этот метод является хорошей иллюстрацией интегрированного подхода, поскольку он обеспечивает комплексную верификацию C-программ, базирующуюся на комбинации операционного, аксиоматического и трансформационного подходов.