Мой рассказ о SAT/SMT летом 2021, часть II

PDF-ка тут: https://smt.st/ 0:52 Сортировочные сети 2:44 Branchless abs() 4:47 Есть ли в 32-битном слове нулевой байт? 5:37 Ф-ция из книги "Beautiful Code": является ли unicode-символ числом? Юзаем CBMC 10:09 Целочисленное переполнение: знаковое и беззнаковое 15:38 Проблемы с two's complement (дополнительный код) 18:20 Массивы в SMT как ITE-деревья 19:26 Uninterpreted functions 19:50 Переизобретаем алгоритм Knuth-Morris-Pratt и верификация при помощи CBMC 26:02 Как KLEE может найти строки попадающие под определенное регулярное выражение 27:11 Решение Судоку при помощи KLEE 31:05 Головоломка про пять домов (Zebra) 33:01 Сборка кубика Рубика 35:02 Головоломка Numberlink, трассировка печатных плат, escape routing 39:06 Генератор кроссвордов 40:10 Nonogram puzzle и дискретная/цифровая томография 41:21 Раскрашивание графов 42:28 Сотовые телефоны 46:40 Распределение регистров в кодегенераторе компилятора 51:20 Задача укладки ранца/рюкзака 53:47 Юзая KLEE, восстанавливаем вход CRC32/64, используя только хеш 56:31 Создаем минимальный набор тестов используя MaxSMT/MaxSAT 59:24 Минимальный набор тестов для электронного девайса 1:01:22 Клики в теории графов 1:06:32 Расселяем студентов в общаге по интересам 1:07:15 Мат.анализ: оптимальная форма пивной банки 1:10:42 x86-ассемблер: выбираем короткие или длинные инструкции перехода (JMP) 1:14:25 Синтез программ 1:19:23 Донгла Rockey, смарткарты 1:25:02 Q&A

Видео Мой рассказ о SAT/SMT летом 2021, часть II автора InkedLegendsLive