Рассмотрена проблема разработки и исследования методов поиска недетерминированного поведения программного обеспечения. Методы верификации программного обеспечения предназначены для подтверждения фактов соответствия конечного программного продукта заявленным требованиям, целью верификации программного обеспечения является обнаружение ошибок, уязвимостей, некорректно реализованных свойств и требований. Существующие методы верификации имеют ряд проблем и недостатков. Предложен синтетический метод верификации программного обеспечения на основе SMT-решателя, позволяющий решить проблему комбинаторного взрыва, охватывающий все заданные свойства проверяемой программы, не требующий построения сложной модели программы. Получен алгоритм работы метода верификации и его реализации на языке SMT-LIB.
展开▼
