Данная статья представляет новый метод статической верификации программного обеспечения, основанный на подходе CEGAR, который нацелен на проверку программы относительно нескольких требований за раз и получение того же результата, который представляет базовый подход, проверяющий требования по отдельности, с учетом того, что каждое требование может нарушаться более одного раза.