# Satisfiability Modulo Theories

## SETSS 2018

 Nikolaj Bjørner Microsoft Research nbjorner@microsoft.com

## Sections

1. An Introduction to Satisfiability Modulo Theories and Z3

2. Theory Solvers

3. SAT and SMT Algorithms

4. Optimization with MaxSAT

5. Quantifier Reasoning

## Bio

• 90's: DTU, DIKU, Stanford
• This is me a week before fixing my thesis topic
• Late 90's: Kestrel Institute
• Early 2000s: XDegrees (file sharing startup)
• 2002-06: Distributed File Replication @ Microsoft
• 2006: MSR: , Network Verification

## Section 1

An Introduction to Satisfiability Modulo Theories and Z3

## Z3

• A state-of-art Satisfiability Modulo Theories (SMT) solver

• On GitHub: https://github.com/Z3prover/z3.git
• Developments: Scalable simplex solver, Strings, Horn clauses, floating points, SAT extensions

## Some Z3 Applications

• Program Verification
• VCC, Everest, Dafny, Havoc, Leon

• Symbolic Execution
• SAGE, Pex, KLEE

• Software Model Checking
• Static Driver Verifier, Smash, SeaHorn

• Configurations
• Network Verification with SecGuru
• Dynamics Product Configuration

## Basic SAT

  Tie, Shirt = Bools('Tie Shirt')
s = Solver()
s.add(Or(Tie, Shirt), Or(Not(Tie), Shirt), Or(Not(Tie), Not(Shirt)))
print s.check()
print s.model()

## Basic SMT

I = IntSort()
f = Function('f', I, I)
x, y, z = Ints('x y z')
A = Array('A',I,I)

fml = Implies(x + 2 == y, f(Select(Store(A, x, 3), y - 2)) == f(y - x + 1))

s = Solver()
print s.check()