В работе рассматривается подход к верификации аллокаторов памяти с применением метода ограниченной проверки моделей. После применения подхода на различных аллокаторах на основании полученной статистики предполагается сделать вывод о наличии уязвимостей, связанных с различными типами ошибок.
Садырин Д.С. (науч. рук. Дергачев А.М.) Формальная верификация аллокаторов памяти с применением символьного выполнения // Сборник тезисов докладов конгресса молодых ученых. Электронное издание. – СПб: Университет ИТМО, [2019]. URL: https://kmu.itmo.ru/digests/article/738