Huawei topics in symbolic execution

[Николай Шилов]

Коллеги,

Как, наверное, вы знаете, Huawei ищет академических партнеров для своих исследовательских проектов, регулярно представляет темы в университетах.

Недавно у нас в Иннополисе была делегация лаборатории Системного программирования Московского центра Huawei. Одна из предложенных ими тем для сотрудничества с "академией" - символическое исполнение. 

Прилагаю к этому письму текст их презентации по этой теме, так как (как мне кажется) она может заинтересовать участников группы. 

Н.В. Шилов

[Arkady Klimov]

Спасибо, Николай. Тема меня немного заинтересовала, чтобы посмотреть, что это за зверь такой - KLEE. Насколько удалось понять (потратив пару-тройку часов), это, если использовать понятия суперкомпиляции - построитель дерева конфигураций, где конфигурация описывается как набор ограничений на переменные состояний. При этом учитываются ссылки, для которых как-то моделируется объект ссылки (состояние фрагмента памяти). Это все работает для С, поскольку проходит через LLVM. Пока я не увидел попыток строить обобщения, не говоря о зацикливаниях. И это очевидная слабость, приводящая к большим переборам: число состояний растет экспоненциально (от длины пути). В частности, проблема 1.1 из списка проблем от Huawei решалась бы на раз при наличии обобщений (не для "зацикливаний", а просто за счет слияния "похожих" состояний, сокращая число рассматриваемых состояний с миллионов до сотен). Возможно, нужно обобщение не автоматическое, а как-то управляемое пользователем.

Достоинства метода в том, что на путях используется решатель для набора ограничений, отсекающий невыполнимые ветви.

Если это скрестить с суперкомпиляцией, можно, наверно, сказать новое слово.

Еще раз спасибо. 

С уважением, 

Аркадий.

пн, 12 апр. 2021 г. в 10:09, Николай Шилов <nikolay....@gmail.com>:

--
Вы получили это сообщение, поскольку подписаны на группу "Метавычисления и специализация программ".
Чтобы отменить подписку на эту группу и больше не получать от нее сообщения, отправьте письмо на электронный адрес metacomputation...@googlegroups.com.
Чтобы посмотреть обсуждение на веб-странице, перейдите по ссылке https://groups.google.com/d/msgid/metacomputation-ru/c09b61fe-ba9a-466e-8d43-b8669f030634n%40googlegroups.com.

--

_______________

С уважением,

Аркадий Климов,
с.н.с. ИППМ РАН,
+7(499)135-32-95
+7(916)072-81-48