Анализ кода с нулевым числом ложных срабатываний в Java с помощью динамического символьного исполнения

В докладе будет показано, как техника динамического символьного исполнения может быть использована для поиска глубоких ошибок в Java без ложных срабатываний. Спикеры классифицируют виды анализа кода и покажет современные техники для этих задач. Раскроют детали реализации символьного исполнения в Java — и вы сможете написать свой собственный анализатор. Спикеры рассмотрят современное состояние дел в этой области, а также покажут простой интерфейс для решения NP-полных задач в вашем Java-приложении — SMT-решатель. В рамках доклада будет возможность закодировать хорошо известные NP-полные задачи (например, Судоку) в SMT на Java, используя самый популярный решатель — Microsoft Z3.

Этот доклад вдохновлен прошлогодним докладом на конференции DotNext.