Личный кабинет
Подробное описание документа
Рудаков И. В.
Разработка и исследование синтетического метода верификации программы с помощью SMT-решателей / Рудаков И. В., Гурин Р. Е. - DOI 10.18698/0236-3933-2016-4-49-64 // Вестник МГТУ им. Н. Э. Баумана. Сер. Приборостроение. - 2016. - № 4. -
Скачать документ
Рассмотрена проблема разработки и исследования методов поиска недетерминированного поведения программного обеспечения. Методы верификации программного обеспечения предназначены для подтверждения фактов соответствия конечного программного продукта заявленным требованиям, целью верификации программного обеспечения является обнаружение ошибок, уязвимостей, некорректно реализованных свойств и требований. Существующие методы верификации имеют ряд проблем и недостатков. Предложен синтетический метод верификации программного обеспечения на основе SMT-решателя, позволяющий решить проблему комбинаторного взрыва, охватывающий все заданные свойства проверяемой программы, не требующий построения сложной модели программы. Получен алгоритм работы метода верификации и его реализации на языке SMT-LIB.
004.3 Аппаратные средства. Техническое обеспечение
Статья опубликована в следующих изданиях
№ 4. - 2016.
