Transcription
Leonardo de Moura and Nikolaj BjørnerMicrosoft Research
Z3 is a Satisfiability Modulo Theories (SMT) solver.Z3 integrates several decision procedures.Z3 is used in several program analysis, verification, testcase generation projects at Microsoft.Z3 1.2 is freely available for academic Z3: An Efficient SMT Solver
x 2 y f (read (write(a, x,3), y 2) f ( y x 1)ArithmeticArray TheoryZ3: An Efficient SMT SolverUninterpretedFunctions
Linear real and integer arithmetic.Fixed-size bit-vectorsUninterpreted functionsExtensional arraysQuantifiersModel generationSeveral input formats (Simplify, SMT-LIB, Z3, Dimacs)Extensive API (C/C , .Net, OCaml)Z3: An Efficient SMT Solver
cationArithmeticArraysE-matchingCore TheoryPartial ordersTuplesSAT solverZ3: An Efficient SMT Solver
Hyper-VVCCHAVOCBug pathRustan Leino, Mike Barnet, Michal Mosƙal, Shaz Qadeer,Shuvendu Lahiri, Herman Venter, Peter Muller,Wolfram Schulte, Ernie CohenZ3: An Efficient SMT SolverBoogieVerificationcondition
Quantifiers, quantifiers, quantifiers, Modeling the runtimeFrame axioms (“what didn’t change”)Users provided assertions (e.g., the array is sorted)Prototyping decision procedures (e.g., reachability, heaps, )Solver must be fast in satisfiable instances.Trade-off between precision and performance.Candidate (Potential) ModelsZ3: An Efficient SMT Solver
Run Test and MonitorseedExecutionPathTestInputsPath ConditionKnownPathsNew inputConstraintSystemSolveUnexplored pathVigilanteNikolai Tillmann, Peli de Halleux, Patrice GodefroidAditya Nori, Jean Philippe Martin, Miguel Castro,Manuel Costa, Lintao ZhangZ3: An Efficient SMT Solver
Formulas may be a big conjunctionPre-processing stepEliminate variables and simplify input formatIncremental: solve several similar formulasNew constraints are asserted.push and pop: (user) backtrackingLemma reuse“Small Models”Given a formula F, find a model M, that minimizes the valueof the variables x0 xnZ3: An Efficient SMT Solver
Z3 is part of SDV 2.0 (Windows 7)It is used for:Predicate abstraction (c2bp)Counterexample refinement (newton)Ella Bounimova, Vlad Levin, Jakob Lichtenberg,Tom Ball, Sriram Rajamani, Byron CookZ3: An Efficient SMT Solver
All-SATFast Predicate AbstractionUnsatisfiable coresWhy the abstract path is not feasible?Z3: An Efficient SMT Solver
Bounded model-checking of model programsTerminationSecurity protocolsBusiness application modelingCryptographyModel Based Testing (SQL-Server)Your killer-application hereZ3: An Efficient SMT Solver
Model-based Theory CombinationHow to efficiently combine theory solvers?Use models to control Theory Combination.E-matching abstract machineTerm indexing data-structures for incremental matchingmodulo equalities.Relevancy propagationUse Tableau advantages with DPLL engineZ3: An Efficient SMT Solver
Given arrays:bool a1[bool];bool a2[bool];bool a3[bool];bool a4[bool];All can be distinct.Add:bool a5[bool];Two of a1,.,a5 mustbe equal.Z3: An Efficient SMT Solver
Coming soon (Z3 2.0):Proofs & Unsat coresSuperposition CalculusDecidable FragmentsMachine LearningNon linear arithmetic (Gröbner Bases)Inductive DatatypesImproved Array & Bit-vector theoriesSeveral performance improvementsMore “customers” & ApplicationsZ3: An Efficient SMT Solver
Z3 is a new SMT solver from Microsoft Research.Z3 is used in several projects.Z3 is freely available for academic Z3: An Efficient SMT Solver
Trade-off between precision and performance. Candidate (Potential) Models Z3: An Efficient SMT Solver. Z3: An Efficient SMT Solver . (SQL-Server) Your killer-application here Z3: An Efficient SMT Solver . modulo equalities. Relevancy propagation Use Tableau advantages with DPLL engine Z3: An Efficient SMT Solver. Z3: An Efficient SMT Solver .
