Синтаксис и операционная семантика целевого языка в реализации технологии «предположи и допусти» при объединении циклов для верификации программ

Loop Fusion – преобразование программы для объединения нескольких последовательных петель в одну – было изучено в основном для оптимизации компилятора. В работе предлагается новая стратегия объединения циклов, которая может объединить любые петли, даже петли с зависимостью данных. Показано, что это полезно для программы проверки, потому что может упростить инварианты цикла. Суть цикла слияния заключается в следующем: если состояние после первого цикла было известно, два тела цикла могут быть вычислены одновременно, независимо от данных путем переименования переменных программы. Loop Fusion создает программу, которая угадывает неизвестное состояние после первого цикла, недетерминированно выполняет слитый цикл, в котором переменные переименовываются, сравнивает угаданное состояние и состояние, фактически вычисленное слитой петлей, и, если они не совпадают, расходится. Последние два шага, сравнение и расхождение, имеют решающее значение для сохранения частичной корректности. Подход «предположи и допусти» назван так потому, что в дополнение к первому шагу (предположи), последние два шага могут быть выражены псевдоинструкцией «допусти», которая используется в проверке программы.

1. Бэкон Д.Ф., Грэм С.Л., Шарп О.Дж. Преобразования компилятора для повышения производительности Вычислительная техника. ACM Comput. Surv. 1994; 26 (4): 345-420.

2. Бейер Д., Керемоглу М.Э. CPAchecker: инструмент для настраиваемой проверки программного обеспечения. CAV 2011 (LNCS). Springer. 2011; 6806: 184-190.

3. Коэн Э. Передача информации в вычислительных системах. ACM SIGOPS Operating Systems Review. ACM. 1977; 11: 133-139.

4. Ферранте Дж., Оттенштейн К.Дж., Уоррен Дж.Д. График зависимости программы и его использование в оптимизации. ACM Trans. Program. Lang. Syst. 1987;9(3):319-349.

5. Гогуэн Дж., Месегер Дж. Политики безопасности и модели безопасности. 1982 Симпозиум IEEE по безопасности и конфиденциальности, Окленд, Калифорния, США. 1982: 11-20.

6. Гурфинкель А., Кахсай Т., Комуравелли А., Навас Дж. А. Схема проверки SeaHorn. CAV 2015 (LNCS), Том. 9206. Springer. 2015: 343-361.

7. Ли П., Зданцевич С. Политика понижения статуса и непринужденное невмешательство. Proc. 32-го Симпозиум ACM SIGPLAN-SIGACT по принципам языков программирования, POPL 2005 г., Лонг-Бич, Калифорния, США. 2005: 158-170.

8. Маклин Дж. Модели безопасности и информационный поток. Симпозиум IEEE по безопасности и конфиденциальности, Окленд, Калифорния, США. 1990: 180-189.

9. Тераучи Т., Айкен А. Защищенный информационный поток как проблема безопасности. Статический анализ, 12th Int. Symposium, SAS 2005, Лондон, Великобритания. 2005: 352-367.

10. Винскель Г. Формальная семантика языков программирования: Введение. Массачусетский технологический институт Пресса. 1993 г.

11. Barnett M., Chang B.-Y.E., DeLine R., Jacobs B., Leino K.R.M. Boogie: Модульный многоразовый верификатор для объектно-ориентированных программ. FMCO 2005 (LNCS). 2005; 4111: 364- 387.

12. Рейнольдс Дж.К. Логика разделения: логика для общих изменяемых структур данных. Симпозиум IEEE по логике в компьютерных науках (LICS’02). 2002 г.