z3
-
Хабрахабр
Парсим строки с SMT-решателем
Этот пост о том, как можно разобрать строку по контектстно-свободной грамматике с помощью SMT-решателя. Здесь будет введение, описание принципа работы и ссылка на github с работающей программой. План поста: Что такое SMT-решатель Формальные грамматики Пример: лямбда-исчисление Правила-суммы Правила-произведения Переводим задачу парсинга на язык SMT-решателя Константы Символы грамматики Группы ячеек Подгруппа ячеек Тип продукции Номер ячейки в группе Формулы Итоги Что…
Читать далее » -
Хабрахабр
Бэкдор АНБ в карманном телексе 1984 года — история повторяется
В музее криптографии Нидерландов представлен интересный экспонат: карманный телекс PX-1000. Он разработан амстердамской фирмой Text Lite, с 1983 года продавался под брендами Philips и др. PX-1000 был рассчитан на журналистов, бизнесменов. Использовался сотрудниками правительстве Нидерландов. Его уникальная особенность — надёжное шифрование по алгоритму DES. Судя по всему, это первый в мире коммуникатор со встроенным шифрованием, выпущенный для массового рынка. Целевая…
Читать далее » -
Хабрахабр
[Из песочницы] Карманное руководство по Z3
Преамбула "Человеческий мозг это пустой чердак. Дурак так и делает: тащит туда нужное и не нужное. И наконец наступает момент, когда самую необходимую вещь туда не запихнешь, или наоборот не достанешь..." В.Б. Ливанов (из к/ф "Шерлок Холмс и доктор Ватсон") Данное руководство не охватывает весь функционал SMT решателя. Оно написано для таких ситуаций, когда человеку срочно нужно вспомнить, подсмотреть как…
Читать далее » -
Хабрахабр
Математическое расследование, как подделывали выборы губернатора в Приморье 16 сентября 2018 года
Во втором туре выборов губернатора Приморского края 16 сентября 2018 года встречались действующий и.о. губернатора Андрей Тарасенко и занявший второе место в первом туре коммунист Андрей Ищенко. В ходе подсчета голосов на сайте ЦИК РФ отображалась информационная панель с растущим числом обработанных протоколов и голосов за кандидатов. 74%) протоколов и не возобновлялась до самого конца. Публикация подробных данных по участкам…
Читать далее » -
Хабрахабр
[Из песочницы] Формальная верификация на примере задачи о волке, козе и капусте
На мой взгляд, в русскоязычном секторе интернета тематика формальной верификации освещена недостаточно, и особенно не хватает простых и наглядных примеров. Я приведу такой пример из зарубежного источника, и дополню собственным решением известной задачи о переправе волка, козы и капусты на другую сторону реки. Но вначале вкратце опишу, что из себя представляет формальная верификация и зачем она нужна. Под формальной верификацией…
Читать далее » -
Хабрахабр
[Перевод] Почему люди не используют формальные методы?
На Software Engineering Stack Exchange я увидел такой вопрос: «Что мешает широкому внедрению формальных методов?» Вопрос был закрыт как предвзятый, а большинство ответов представляли собой комментарии типа «Слишком дорого!!!» или «Сайт — это не самолёт!!!» В каком-то смысле это верно, но мало что объясняет. Я написал эту статью, чтобы дать более широкую историческую картину формальных методов (FM), почему они на…
Читать далее » -
Хабрахабр
Triton vs Kao’s Toy Project. Продолжаем хорошую традицию
В данной статье речь пойдет про SMT-решатели. Так сложилось, что в исследовательских материалах, посвященных данной теме, появилась хорошая традиция. Уже несколько раз в качестве подопытного алгоритма для SMT-решателей разные исследователи выбирали один и тот же пример – крякми, придуманное некогда человеком с ником kao. Что ж, продолжим эту традицию и попробуем использовать для решения этого крякми еще один инструмент для…
Читать далее »