Лаборатория языковых инструментов

Символьное исполнение (symbolic execution) - это метод анализа программ, основанный на решении задачи выполнимости формул в теориях (satisfiability modulo theories), в котором программа исполняется с символьными переменными вместо конкретных значений, а результатом исполнения являются формулы над этими символьными переменными. Символьное исполнение имеет множество применений, включая поиск ошибок и уязвимостей, генерацию тестов, верификацию, и т.д. В первой части доклада будут описаны проблемы традиционного символьного исполнения и некоторые алгоритмические и инженерные подходы к их решению. Во второй части доклада будет представлено расширение символьного исполнения для логики второго порядка, которое позволяет решать более сложные задачи, такие как автоматическое исправление ошибок и моделирование среды исполнения.

Материалы к докладу:

1. Cristian Cadar, Daniel Dunbar, Dawson Engler. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs // OSDI 2008
2. Edward J. Schwartz, Thanassis Avgerinos, David Brumley. All You Ever Wanted to Know about Dynamic Taint Analysis and Forward Symbolic Execution (but Might Have Been Afraid to Ask) // S&P 2010
3. Sergey Mechtaev, Alberto Griggio, Alessandro Cimatti, Abhik Roychoudhury. Symbolic Execution with Existential Second-Order Constraints // FSE 2018

Докладчик: Сергей Мечтаев, University College of London