| |
Мандрыкин, М. У.
Анализ регионов для дедуктивной верификации Си-прграмм [Текст] / М. У. Мандрыкин, А. В. Хорошилов
// Программирование. – 2016. – № 5. – С. 3-29.
В статье предложена модель памяти с разделением на непересекающиеся области, предназначенная для дедуктивной верификации Си-программ. Определена семантика базового языка, описаны нормализующие преобразования, позволяющие преобразовать исходную аннотированную Си-программу в соответствующую программу на базовом языке. |
