Max Home IndustryУстройство доказательства теорем Z3 от Microsoft Research было удостоено награды ACM SIGPLAN Programming Languages за 2015 год.
Премия присуждается за
«Разработка системы программного обеспечения, которая имела длительное влияние, отраженное в вкладе в концепции, в коммерческом признании или в том и другом».
Объявление состоялось во время PLDI 2015, ежегодной конференции ACM SIGPLAN по проектированию и реализации языков программирования. Z3 — это решатель SMT.
SMT расшифровывается как «Теории выполнимости по модулю».
Это сложная идея, которую лучше всего объяснять по частям, начиная с «Теорий». Предположим, у вас есть теорема, которую вы хотите проверить, в которой логические формулы в теореме могут принимать несколько значений. Что вам нужно, так это какой-нибудь автоматический способ показать, можно ли доказать истинность теоремы, выбрав конкретные значения для переменных в вашей теореме, конечные или бесконечные.
Более понятные приложения могут быть целочисленными арифметическими или бесплатными функциями. На практике такие лежащие в основе теории используются в моделях предметной области, где требуется доказательство теорем.
Примерами могут быть обнаружение условий, которые должны быть выполнены для того, чтобы приложение использовало определенный путь кода; будет ли блок кода никогда не запускаться; или могут ли некоторые свойства одновременно быть истинными, что указывает на ошибку.
Так как же удовлетворить теорию?
Метод грубой силы состоит в том, чтобы составить таблицу истинности, содержащую все возможные входные данные, которые меняются, с конечным результатом, но любой, кто сделал это для небольшого числа переменных, знает, как быстро таблица становится неуправляемой.
Обычно мы хотим знать, верна ли когда-либо определенная формула в данной теории.
Это то, что называется выполнимостью.
Часть названия Modulo означает «при наличии определенных теорий».
Z3 — это реализация решателя SMT от Microsoft — автоматизированная альтернатива, позволяющая показать, может ли когда-либо быть удовлетворена теория. В Microsoft разработчики использовали Z3 для поиска уязвимостей.
Они приняли более миллиарда ограничений, созданных Sage (фаззер белого ящика Microsoft, метод систематического выявления уязвимостей безопасности. Sage работает так, что приложение запускается с первыми входными данными. Sage собирает ограничения для входных данных в условных операторах, а затем использует решатель ограничений для создания новых тестовых входных данных).
Microsoft заявляет, что Sage сэкономил компании миллионы долларов, которые были бы потрачены на исправление ошибок в поставляемых продуктах. Z3 также обеспечивает основу для средства проверки политики безопасности облачных сервисов, инструмента создания тестовых примеров Pex, проверяющего компилятора C и обнаружения вредоносных программ JavaScript, среди прочего.
Z3 стал открытым исходным кодом по лицензии MIT в марте. Он поддерживает Windows, OSX, Linux и FreeBSD, и с момента выпуска кода в октябре 2012 года он был загружен более 20 000 раз. Вы также можете вызвать Z3 процедурно, используя различные API, доступные в C, C ++, Java, .Net, OCaml и Python. Вы можете попробовать Z3 в своем браузере на Rise4Fun.