Направляемый свойством поиск реляционных инвариантов

Достижимость, направляемая свойством, (Property Directed Reachability, PDR) — эффективный и масштабируемый подход к решению систем символьных ограничений, известных как дизъюнкты Хорна с ограничениями (Constrained Horn Clauses, CHC). В случае нелинейных систем дизъюнктов, которые могут возникнуть, к примеру, из задач реляционной верификации, PDR выводит индуктивные инварианты для каждого неинтерпретированного предикатного символа. Тем не менее на практике автоматический вывод таких решений не удаётся, т.к. инварианты должны выводиться для групп предикатных символов вместо индивидуальных предикатных символов. В статье описан новый алгоритм, автоматически определяющий такие группы и обобщающий существующий подход PDR. Ключевая особенность алгоритма состоит в том, что он не требует потенциально дорогой синхронизирующей трансформации системы дизъюнктов Хорна. Алгоритм был реализован над современным решателем дизъюнктов Хорна Spacer. Эксперименты показывают, что полученная реализация успешно выводит реляционные инварианты для некоторых систем дизъюнктов, на которых существующие решатели не завершаются.