3. Фундаментальные и технологические проблемы информационных, телекоммуникационных и вычислительных систем
Программа 3.3. Архитектура, системные решения и программно-аппаратное обеспечение информационно-вычислительных комплексов новых поколений — распределенные вычисления, распределенные высокопроизводительные вычислительные ресурсы, параллельные вычисления, системы массового параллелизма, программное обеспечение

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