Z3 Theorem Prover es un solucionador de teorías de módulo de satisfacibilidad (SMT) multiplataforma de Microsoft . [2]
Autor (es) original (es) | Investigación de Microsoft |
---|---|
Desarrollador (es) | Microsoft |
Versión inicial | 2012 |
Lanzamiento estable | z3-4.8.10 / 20 de enero de 2021 [1] |
Repositorio | github |
Escrito en | C ++ |
Sistema operativo | Windows , FreeBSD , Linux ( Debian , Ubuntu ), macOS |
Plataforma | IA-32 , x86-64 |
Tipo | Demostrador de teoremas |
Licencia | Licencia MIT |
Sitio web | github |
Descripción general
Z3 fue desarrollado en el grupo de Investigación en Ingeniería de Software (RiSE) en Microsoft Research y está dirigido a resolver problemas que surgen en la verificación y el análisis de software . Z3 admite aritmética, vectores de bits de tamaño fijo, matrices extensionales, tipos de datos, funciones no interpretadas y cuantificadores. Sus principales aplicaciones son la verificación estática extendida, la generación de casos de prueba y la abstracción de predicados.
En 2015, recibió el Premio al Software de Lenguajes de Programación de ACM SIGPLAN . [3] [4] En 2018, Z3 recibió el premio Test of Time de las conferencias conjuntas europeas sobre teoría y práctica del software (ETAPS). [5] Los investigadores de Microsoft Nikolaj Bjørner y Leonardo de Moura recibieron el Premio Herbrand 2019 por Contribuciones Distinguidas al Razonamiento Automatizado en reconocimiento a su trabajo para avanzar en la demostración de teoremas con Z3. [6] [7]
Z3 fue de código abierto a principios de 2015. [8] El código fuente tiene licencia MIT y está alojado en GitHub . [9] El solucionador se puede construir usando Visual Studio , un Makefile o usando CMake y se ejecuta en Windows , FreeBSD , Linux y macOS .
Tiene enlaces para varios lenguajes de programación, incluidos C , C ++ , Java , Haskell , OCaml , Python , WebAssembly y .NET / Mono . El formato de entrada predeterminado es SMTLIB2 .
Ejemplos de
Lógica proposicional y de predicados
En este ejemplo, las afirmaciones de lógica proposicional se verifican utilizando funciones para representar las proposiciones ay b. El siguiente script Z3 comprueba si:
(declarar divertido a () Bool)(declarar divertido b () Bool)(afirmar (no (= (no (y ab)) (o (no a) (no b)))))(check-sat)
Resultado:
insatisfecho
Tenga en cuenta que el guión afirma la negación de la proposición de interés. Los UNSAT medios resultado de que la proposición negada no es satisfiable, lo que demuestra el resultado deseado ( leyes de De Morgan ).
Resolver ecuaciones
El siguiente script resuelve las dos ecuaciones dadas, encontrando valores adecuados para las variables ayb:
(declare-const a Int)(declare-const b Int)(afirmar (= (+ ab) 20))(afirmar (= (+ a (* 2 b)) 10))(check-sat)(obtener modelo)
Resultado:
se sentó(modelo (define-fun b () Int -10) (define-fun a () Int 30))
Ver también
- Verificación formal
- Alt-Ergo
Referencias
- ^ https://github.com/Z3Prover/z3/releases/tag/z3-4.8.10
- ^ http://lim.univ-reunion.fr/staff/fred/Enseignement/AlgoAvancee/Exos/Z3-exercises.pdf
- ^ "Premio al software de lenguajes de programación" . www.sigplan.org .
- ^ Microsoft Z3 Theorem Prover gana el premio
- ^ Premio ETAPS 2018 Test of Time
- ^ La magia interior detrás del demostrador del teorema Z3 - Microsoft Research
- ^ Premio Herbrand
- ^ "Línea de tiempo de Visual Studio de Microsoft y prueba de teoremas Z3, Google Cloud Launcher, resumen de noticias Fresco-SD Times de Facebook: 27 de marzo de 2015" . 27 de marzo de 2015.
- ^ "GitHub - Z3Prover / z3: The Z3 Theorem Prover" . 1 de diciembre de 2019 - a través de GitHub.
Otras lecturas
- Leonardo De Moura, Nikolaj Bjørner (2008). "Z3: un solucionador SMT eficiente". Herramientas y algoritmos para la construcción y análisis de sistemas . 4963 : 337–340.Mantenimiento de CS1: utiliza el parámetro de autores ( enlace )
- Dennis Yurichev - SAT / SMT por ejemplo - Con muchos ejemplos usando Z3Py.
enlaces externos
- Página web oficial
- La magia interior detrás del demostrador del teorema Z3
- Z3 @ rise4fun de Microsoft