Статья «Проверка нескольких требований за один запуск инструмента статической верификации с помощью CEGAR, "Программирование"»

На данный момент статические верификаторы, основанные на уточнении абстракции по контрпримерам - подходе CEGAR (Counterexample Guided Abstraction Refinement), могут доказывать корректность программы относительно заданного требования, находить его нарушение в программе, при этом останавливая анализ. Или завершать анализ без получения ответа на вопрос, нарушается ли требование в программе или нет, например, при расходовании всех имеющихся ресурсов. Теоретически возможно использовать подход CEG AR для проверки программы относительно нескольких требований за раз, однако при этом нахождение первого нарушения требования или невозможность доказательства его корректности приведет к тому, что мы не сможем проверить программу относительно других требований. Кроме того, если программа содержит более одного нарушения заданного требования, то с помощью подхода CEGAR можно найти только первое нарушение. В данных случаях мы можем пропустить потенциальные ошибки в программе. В то же самое время статические верификаторы выполняют одинаковые действия во время проверки одной и той же программы относительно разных требований и, таким образом, большое количество вычислительных ресурсов тратится впустую. Помимо этого, для нахождения других нарушений заданного требования необходимо сначала исправить найденное, а потом полностью повторить верификацию. Данная статья представляет новый метод статической верификации программного обеспечения, основанный на подходе CEGAR, который нацелен на проверку программы относительно нескольких требований за раз и получение того же результата, который предоставляет базовый подход, проверяющий требования по отдельности, с учетом того, что каждое требование может нарушаться более одного раза. Для того чтобы добиться этого, предложенный метод разделяет ресурсы для проверки различных требований и продолжает анализ после нахождения нарушения требования. Мы использовали модули ядра Linux для проведения экспериментов, в которых предложенный метод позволил сократить общее время верификации в 5 раз. При этом общее число различающихся результатов в сравнении с базовым CEGAR составило порядка 2%. При продолжении анализа после нахождения первого нарушения требования данный метод позволяет гарантировать, что почти в 40% случаев найдены все имеющиеся нарушения заданных требований, при этом находится примерно в 1.5 раза больше нарушений, чем в базовом подходе CEGAR.