z3

  • ХабрахабрФото Парсим строки с SMT-решателем

    Парсим строки с SMT-решателем

    Этот пост о том, как можно разобрать строку по контектстно-свободной грамматике с помощью SMT-решателя. Здесь будет введение, описание принципа работы и ссылка на github с работающей программой. План поста: Что такое SMT-решатель Формальные грамматики Пример: лямбда-исчисление Правила-суммы Правила-произведения Переводим задачу парсинга на язык SMT-решателя Константы Символы грамматики Группы ячеек Подгруппа ячеек Тип продукции Номер ячейки в группе Формулы Итоги Что…

    Читать далее »
  • ХабрахабрФото Бэкдор АНБ в карманном телексе 1984 года — история повторяется

    Бэкдор АНБ в карманном телексе 1984 года — история повторяется

    В музее криптографии Нидерландов представлен интересный экспонат: карманный телекс PX-1000. Он разработан амстердамской фирмой Text Lite, с 1983 года продавался под брендами Philips и др. PX-1000 был рассчитан на журналистов, бизнесменов. Использовался сотрудниками правительстве Нидерландов. Его уникальная особенность — надёжное шифрование по алгоритму DES. Судя по всему, это первый в мире коммуникатор со встроенным шифрованием, выпущенный для массового рынка. Целевая…

    Читать далее »
  • ХабрахабрФото [Из песочницы] Карманное руководство по Z3

    [Из песочницы] Карманное руководство по Z3

    Преамбула "Человеческий мозг это пустой чердак. Дурак так и делает: тащит туда нужное и не нужное. И наконец наступает момент, когда самую необходимую вещь туда не запихнешь, или наоборот не достанешь..." В.Б. Ливанов (из к/ф "Шерлок Холмс и доктор Ватсон") Данное руководство не охватывает весь функционал SMT решателя. Оно написано для таких ситуаций, когда человеку срочно нужно вспомнить, подсмотреть как…

    Читать далее »
  • ХабрахабрФото Математическое расследование, как подделывали выборы губернатора в Приморье 16 сентября 2018 года

    Математическое расследование, как подделывали выборы губернатора в Приморье 16 сентября 2018 года

    Во втором туре выборов губернатора Приморского края 16 сентября 2018 года встречались действующий и.о. губернатора Андрей Тарасенко и занявший второе место в первом туре коммунист Андрей Ищенко. В ходе подсчета голосов на сайте ЦИК РФ отображалась информационная панель с растущим числом обработанных протоколов и голосов за кандидатов. 74%) протоколов и не возобновлялась до самого конца. Публикация подробных данных по участкам…

    Читать далее »
  • ХабрахабрФото [Из песочницы] Формальная верификация на примере задачи о волке, козе и капусте

    [Из песочницы] Формальная верификация на примере задачи о волке, козе и капусте

    На мой взгляд, в русскоязычном секторе интернета тематика формальной верификации освещена недостаточно, и особенно не хватает простых и наглядных примеров. Я приведу такой пример из зарубежного источника, и дополню собственным решением известной задачи о переправе волка, козы и капусты на другую сторону реки. Но вначале вкратце опишу, что из себя представляет формальная верификация и зачем она нужна. Под формальной верификацией…

    Читать далее »
  • ХабрахабрФото [Перевод] Почему люди не используют формальные методы?

    [Перевод] Почему люди не используют формальные методы?

    На Software Engineering Stack Exchange я увидел такой вопрос: «Что мешает широкому внедрению формальных методов?» Вопрос был закрыт как предвзятый, а большинство ответов представляли собой комментарии типа «Слишком дорого!!!» или «Сайт — это не самолёт!!!» В каком-то смысле это верно, но мало что объясняет. Я написал эту статью, чтобы дать более широкую историческую картину формальных методов (FM), почему они на…

    Читать далее »
  • ХабрахабрФото Triton vs Kao’s Toy Project. Продолжаем хорошую традицию

    Triton vs Kao’s Toy Project. Продолжаем хорошую традицию

    В данной статье речь пойдет про SMT-решатели. Так сложилось, что в исследовательских материалах, посвященных данной теме, появилась хорошая традиция. Уже несколько раз в качестве подопытного алгоритма для SMT-решателей разные исследователи выбирали один и тот же пример – крякми, придуманное некогда человеком с ником kao. Что ж, продолжим эту традицию и попробуем использовать для решения этого крякми еще один инструмент для…

    Читать далее »


Кнопка «Наверх»