Z3: An Efficient SMT Solver
Leonardo de Moura and Nikolaj Bjørner
Microsoft Research
•
Z3 is a
Satisfiability Modulo Theories (SMT)
solver.
•
Z3 integrates several decision procedures.
•
Z3 is used in several program analysis, verification, test-
case generation projects at Microsoft.
•
Z3 1.2 is freely available for academic research:
•http://research.microsoft.com/projects/z3
Z3: An Efficient SMT Solver
Z3: An Efficient SMT Solver
•
Linear real and integer arithmetic.
•
Fixed-size bit-vectors
•
Uninterpreted functions
•
Extensional arrays
•
Quantifiers
•
Model generation
•
Several input formats (Simplify, SMT-LIB, Z3, Dimacs)
•
Extensive API (C/C++, .Net, OCaml)
Z3: An Efficient SMT Solver
Z3: An Efficient SMT Solver
Theories
Core Theory
SAT solver
Rewriting
Simplification
Bit-Vectors
Arithmetic
Partial orders
Tuples
E-matching
Arrays
OCaml
Text
.NET
C
Z3: An Efficient SMT Solver
VCC
Boogie
Hyper-V
Rustan Leino, Mike Barnet, Michal Mosƙal, Shaz Qadeer,
Shuvendu Lahiri, Herman Venter, Peter Muller,
Wolfram Schulte, Ernie Cohen
Verification
condition
Bug path
HAVOC
•
Quantifiers, quantifiers, quantifiers, …
•
Modeling the runtime
•
Frame 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) Models
Z3: An Efficient SMT Solver
Z3: An Efficient SMT Solver
Execution
Execution
Path
Path
Run Test and Monitor
Path Condition
Unexplored path
Solve
seed
New input
Test
Test
Inputs
Inputs
Nikolai Tillmann, Peli de Halleux, Patrice Godefroid
Aditya Nori, Jean Philippe Martin, Miguel Castro,
Manuel Costa, Lintao Zhang
Constraint
Constraint
System
System
Known
Known
Paths
Paths
Vigilante
•
Formulas may be a big conjunction
•
Pre-processing step
•
Eliminate variables and simplify input format
•
Incremental: solve several similar formulas
•
New constraints are asserted.
•
push
and
pop
: (user) backtracking
•
Lemma reuse
•
“Small Models”
•
Given a formula
F
, find a model
M
, that minimizes the value
of the variables
x
0
… x
n
Z3: An Efficient SMT Solver
Z3: An Efficient SMT Solver
Ella Bounimova, Vlad Levin, Jakob Lichtenberg,
Tom Ball, Sriram Rajamani, Byron Cook
•
Z3 is
part of SDV 2.0 (Windows 7)
•
It
is used for:
•
Predicate abstraction (c2bp)
•
Counterexample refinement (newton)
•
All-SAT
•
Fast Predicate Abstraction
•
Unsatisfiable cores
•
Why the abstract path is not feasible?
Z3: An Efficient SMT Solver
•
Bounded model-checking of model programs
•
Termination
•
Security protocols
•
Business application modeling
•
Cryptography
•
Model Based Testing (SQL-Server)
•
Your killer-application here
Z3: An Efficient SMT Solver
•
Model-based Theory Combination
•
How to efficiently combine theory solvers?
•
Use models to control Theory Combination.
•
E-matching abstract machine
•
Term indexing data-structures for incremental matching
modulo equalities.
•
Relevancy propagation
•
Use Tableau advantages with DPLL engine
Z3: An Efficient SMT Solver
Z3: 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 must
be equal.
•
Coming soon (Z3 2.0):
•
Proofs & Unsat cores
•
Superposition Calculus
•
Decidable Fragments
•
Machine Learning
•
Non linear arithmetic (Gröbner Bases)
•
Inductive Datatypes
•
Improved Array & Bit-vector theories
•
Several performance improvements
•
More “customers” & Applications
Z3: 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 research:
•
http://research.microsoft.com/projects/z3
Z3: An Efficient SMT Solver
© 2007 Microsoft Corporation. All rights reserved. Microsoft, Windows, Windows Vista and other product names are or may be registered trademarks and/or trademarks in the U.S. and/or other countries.
The information herein is for informational purposes only and represents the current view of Microsoft Corporation as of the date of this presentation. Because Microsoft must respond to changing market conditions, it should not be interpreted to be a commitment on the part of Microsoft, and Microsoft cannot guarantee the accuracy of any information provided after the date of this presentation.
MICROSOFT MAKES NO WARRANTIES, EXPRESS, IMPLIED OR STATUTORY, AS TO THE INFORMATION IN THIS PRESENTATION.
Z3 is an efficient Satisfiability Modulo Theories (SMT) solver that integrates various decision procedures for program analysis, verification, and test case generation. It supports linear arithmetic, bit-vectors, uninterpreted functions, quantifiers, and offers an extensive API for different programming languages. Z3's core components include theories, text, bit-vectors, rewriting, and more. It finds applications in program verification, test case generation, and modeling runtime frame axioms. Notable clients include Hyper-V, Boogie, and VCC.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Z3: An Efficient SMT Solver Leonardo de Moura and Nikolaj Bj rner Microsoft Research
Overview Z3 is a Satisfiability Modulo Theories (SMT) solver. Z3 integrates several decision procedures. Z3 is used in several program analysis, verification, test- case generation projects at Microsoft. Z3 1.2 is freely available for academic research: http://research.microsoft.com/projects/z3 Z3: An Efficient SMT Solver
Satisfiability Modulo Theories (SMT) + = = ) 1 + 2 ( ( ( , 3 , x ), ) 2 ( x y f read write a y f y x Uninterpreted Arithmetic Array Theory Functions Z3: An Efficient SMT Solver
Main features Linear real and integer arithmetic. Fixed-size bit-vectors Uninterpreted functions Extensional arrays Quantifiers Model generation Several input formats (Simplify, SMT-LIB, Z3, Dimacs) Extensive API (C/C++, .Net, OCaml) Z3: An Efficient SMT Solver
Z3: Core System Components Theories Text C .NET OCaml Bit-Vectors Rewriting Simplification Arithmetic Arrays Core Theory E-matching Partial orders Tuples SAT solver Z3: An Efficient SMT Solver
Clients: Program Verification Hyper-V Boogie VCC Verification condition Win. Modules HAVOC Bug path Rustan Leino, Mike Barnet, Michal Mos al, Shaz Qadeer, Shuvendu Lahiri, Herman Venter, Peter Muller, Wolfram Schulte, Ernie Cohen Z3: An Efficient SMT Solver
Z3 & Program Verification Quantifiers, quantifiers, quantifiers, Modeling the runtime Frame 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) Models Z3: An Efficient SMT Solver
Clients: Test case generation Run Test and Monitor Path Condition Execution Path Test Inputs seed Known Paths New input Constraint System Solve Unexplored path Vigilante Nikolai Tillmann, Peli de Halleux, Patrice Godefroid Aditya Nori, Jean Philippe Martin, Miguel Castro, Manuel Costa, Lintao Zhang Z3: An Efficient SMT Solver
Z3 & Test case generation Formulas may be a big conjunction Pre-processing step Eliminate variables and simplify input format Incremental: solve several similar formulas New constraints are asserted. push and pop: (user) backtracking Lemma reuse Small Models Given a formula F, find a model M, that minimizes the value of the variables x0 xn Z3: An Efficient SMT Solver
Client: Static Driver Verifier 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 Cook Z3: An Efficient SMT Solver
Z3 & Static Driver Verifier All-SAT Fast Predicate Abstraction Unsatisfiable cores Why the abstract path is not feasible? Z3: An Efficient SMT Solver
More Microsoft clients Bounded model-checking of model programs Termination Security protocols Business application modeling Cryptography Model Based Testing (SQL-Server) Your killer-application here Z3: An Efficient SMT Solver
Some Technical goodies Model-based Theory Combination How to efficiently combine theory solvers? Use models to control Theory Combination. E-matching abstract machine Term indexing data-structures for incremental matching modulo equalities. Relevancy propagation Use Tableau advantages with DPLL engine Z3: An Efficient SMT Solver
Example: C API 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 must be equal. Z3: An Efficient SMT Solver
Future/Current Work Coming soon (Z3 2.0): Proofs & Unsat cores Superposition Calculus Decidable Fragments Machine Learning Non linear arithmetic (Gr bner Bases) Inductive Datatypes Improved Array & Bit-vector theories Several performance improvements More customers & Applications Z3: An Efficient SMT Solver
Conclusions Z3 is a new SMT solver from Microsoft Research. Z3 is used in several projects. Z3 is freely available for academic research: http://research.microsoft.com/projects/z3 Z3: An Efficient SMT Solver
