# Quantified Satisfiability Modulo Theories

## 2nd SAT+SMT School, Mysore, December 2017

 Nikolaj Bjørner Microsoft Research nbjorner@microsoft.com

## 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

## Quantifier Engines in Z3

•  E-matching

• [5, 11, 29, 36] Model-based Quantifier Instantiation (MBQI)

• [1, 2, 31] Quantifier Elimination and Satifiability

• [4, 13] Horn Clauses

• Deprecated:  EPR using relational algebra,  Superposition, see also VampireZ3

## E-matching and Pattern based quantifier instantiation 

• Smallest subterm containing :
• Use ground equality to match with .
• Formulas are ground unsatisfiable.

### E-matching - efficiency

• Secret sauce is to find instantiations
• quickly,
• across large sets of terms, and
• incrementally.

### E-matching - basic algorithm

Takes

• a ground term,
• a pattern that may contain variables, and
• a congruence closure structre cc that for each ground term represents an equivalence class of terms that are congruet in the current context.

### E-matching - a primer on congruence closure

• Let be a set of terms and set of equalities over .

• A congruence closure over modulo is the finest a partition of , cc, such that:

• if , then are in the same partition in cc.

• for ,

• if are in same partition of cc for each , then
• are in the same partition under cc.
• Convention: , maps term to its equivalence class.

### E-matching - basic algorithm, code

def match(pattern, term, $\theta$, cc):
pattern = pattern$\theta$
if pattern == term:
yield $\theta$
elif is_var(pattern):
yield $\theta[$pattern$\mapsto$ term$]$
else:
f(patterns) = pattern
for f(terms) in cc(term):
# e.g., with same head function symbol f
for $\theta'$ in matches(patterns, terms, $\theta$, cc):
yield $\theta'$

def matches(patterns, terms, $\theta$, cc):
if not patterns:
yield $\theta$
return
for $\theta'$ in match(patterns, terms, $\theta$, cc):
for $\theta''$ in matches(patterns[1:], terms[1:], $\theta'$, cc):
yield $\theta''$

### E-matching - beyond the basic algorithm

• Match is invoked for every pattern in database.
• To avoid common work:
• Compile set of patterns into instructions.
• By partial evaluation of naive algorithm
• Instruction sequences share common sub-terms.
• Substitutions are stored in registers,

### E-matching - code trees (0)

PC Instruction
init(f, ) add arguments of to registers 1-4
check(4,,) check if is congruent to
bind(2, , 5, ) bind terms in with to
compare(1, 5, ) check if equals
check(6, , ) check if is congruent to
bind(3, , 7, ) bind terms in with to
yield(1,7) output binding from

PC Instruction
init(f, )
check(4,,)
bind(2, , 5, )
compare(1, 5, )
check(6, , )
bind(3, , 7, )
yield(1,7)

PC Instruction
init(f, )
check(4,,)
bind(2, , 5, )
compare(1, 5, )
check(6, , )
bind(3, , 7, )
yield(1,7)

### E-matching abstract machine ### E-matching abstract machine - NB

• Patterns that share common (top-down) term structure can share code sequences.

• This saves on common work.

• Use the choice instruction to branch when patterns end up having different sub-terms.

• Other instructions are possible,

• forward pruning: lookahead multiple function symbols in immediate subterms before diving into any subterm.

• to deal with multi-patterns, when maching more than one pattern at a time.

### Inverted path indexing

• During search, congruence classes are merged.

• Q: Which merges could enable pattern to be matched?

• A: When pattern contains term , and

• a node is in in the same class as a node labeled by ,

• a node is an argument of in the same position as ,

• , are merged

• Idea: Build an index of all pairs from patterns.

• during a merge with look for matches in index.

## Model-based Quantifier Instantiation [5, 11, 29, 36]

Check

while is SAT with model :
if is UNSAT return SAT
model for
find , such that .

return UNSAT

where is partially evaluated using interpretation .

### Partial model evaluation

• is partially evaluated using interpretation .

Example:

### Model-based Quantifier Instantiation - scope

Quite powerful when search space for instantiation terms is finite

• EPR, UFBV, Array property fragment, Essentially UF
• Combine with template space

### EPR

Also known as Bernays-Schoenfinkel-Ramsey class.

Same complexity as DQBF.

### EPR Example

(declare-sort T)

(declare-fun subtype (T T) Bool)

;; subtype is reflexive
(assert (forall ((x T)) (subtype x x)))

;; subtype is antisymmetric
(assert (forall ((x T) (y T))  (=> (and (subtype x y) (subtype y x)) (= x y))))

;; subtype is transitive
; ...

;; subtype has the tree-property
(assert (forall ((x T) (y T) (z T))
(=> (and (subtype x z) (subtype y z)) (or (subtype x y) (subtype y x)))))

;; we have an additional axiom: every type is a subtype of obj-type
(declare-const obj-type T) ....
(assert (forall ((x T)) (subtype x obj-type)))

(assert (subtype int-type real-type))
(assert (subtype real-type complex-type))
(assert (not (subtype string-type real-type)))

### EPR decidability

• Skolemize
• , the are free constants
• Instantiate
• where ranges over all bindings of to .
• Check ground SAT
• Ground SAT implies finite model of size at most .

### EPR using MBQI

• Skolemize

• , the are free constants
• Models for bind variables to free constants

• The number of possible such models is bounded by .

### UFBV Example

(set-option :smt.mbqi true)
(define-sort Char () (_ BitVec 8))

(declare-fun f  (Char) Char)
(declare-fun f1 (Char) Char)
(declare-const a Char)

(assert (bvugt a #x00))
(assert (= (f1 (bvadd a #x01)) #x00))
(assert (forall ((x Char)) (or (= x (bvadd a #x01)) (= (f1 x) (f x)))))

(check-sat)
(get-model)

### UFBV decidability

• All variables range over finite domains.

• Quantifier-free fragment is not only NP hard, it is NEXPTIME hard.

• QF-UFBV can be encoded into EPR. 
• Quantified fragment is another complexity jump.

• BV - quantifier elimination 

• UFBV using MBQI 

• Use templates to find general instances

### Map Property Fragment - Example

• is equal to except at index .

• can only have two values, or .

### Array Property Example

(set-option :smt.mbqi true)
(set-option :model.compact true)

;; A0, A1, A2, A3, A4 are "arrays" from Integers to Integers.
(declare-fun A0 (Int) Int) (declare-fun A1 (Int) Int)
(declare-fun A2 (Int) Int) (declare-fun A3 (Int) Int)
(declare-fun A4 (Int) Int)
(declare-const n Int) (declare-const l Int)
(declare-const k Int) (declare-const x Int)
(declare-const y Int) (declare-const w Int)
(declare-const z Int)

;; A1 = A0[k <- w]
(assert (= (A1 k) w))
(assert (forall ((x Int)) (or (= x k) (= (A1 x) (A0 x)))))

;; A2 = A1[l <- x] = A0[k <- w][l <- x]
(assert (= (A2 l) x))
(assert (forall ((x Int)) (or (= x l) (= (A2 x) (A1 x)))))

;; A3 = A0[k <- y]
(assert (= (A3 k) y))
(assert (forall ((x Int)) (or (= x k) (= (A3 x) (A0 x)))))

;; A4 = A3[l <- z] = A0[k <- y][l <- z]
(assert (= (A3 l) z))
(assert (forall ((x Int)) (or (= x l) (= (A4 x) (A3 x)))))

(assert (and (< w x) (< x y) (< y z)))
(assert (and (< 0 k) (< k l) (< l n)))
(assert (> (- l k) 1))

;; A2 is sorted in the interval [0,n-1]
(assert (forall ((i Int) (j Int))
(=> (and (<= 0 i) (<= i j) (<= j (- n 1)))
(<= (A2 i) (A2 j)))))

(check-sat)
(get-model)

;; A4 is sorted in the interval [0,n-1]
(assert (forall ((i Int) (j Int))
(=> (and (<= 0 i) (<= i j) (<= j (- n 1)))
(<= (A4 i) (A4 j)))))

(check-sat)

### Array property Fragment - sufficient instantiations

• Given formula with free.

• Let be set of a set of from .

Definition 1.
The set is a sufficient set of instances for , if

• In other words, for every possible instantiation of there is a that satisfies at least the same combination of guards.

### Array Property Fragment - arithmetic

Proposition 1.
If admits a finite sufficient set of instances , it can be evaluated using those.

Proposition 2.
Formulas in the array and map property fragments admit a sufficient set of instantiations.

Proposition 3.
MBQI is a decision procedure the array and map property fragments by using the instantiation sets computed from the formulas.

### Essentially Uninterpreted Fragment 

Synthesize generalized instantiation sets using grammar rules.

Applies to winder range of formulas than the syntactic array property fragment.

• list property fragment by McPeak and Necula
• several locally finite theories - Stokkermans et. al.

### Essentially Uninterpreted Example

(set-option :smt.mbqi true)
;; f an g are "streams"
(declare-fun f (Int) Int)
(declare-fun g (Int) Int)

;; the segment [a, n + a] of stream f is equal to the segment [0, n] of stream g.
(declare-const n Int)
(declare-const a Int)
(assert (forall ((x Int)) (=> (and (<= 0 x) (<= x n))
(= (f (+ x a)) (g x)))))

;; adding some constraints to a
(assert (> a 10))
(assert (>= (f a) 2))
(assert (<= (g 3) (- 10)))

(check-sat)
(get-model)

### Instantiation sets and Quantifiers

• As pursued in 

• The notion of instantiation set can be extended along a different dimension of virtual substitutions.

• Several theories admit quantifier elimination by virtual substitutions.

• Example .

• Tricky part: ensure that set of virtual substitutions does not grow unbounded.

## QSAT 

### Instantiations from repeated SMT calls 

Goal: To find a quantifier free , such that

Tool: project that eliminates from a conjunction
that is, project() .

Initialize:

Repeatedly: find conjunctions that imply

Update: project().

### Instantiations - Algorithm

def qe($\exists \vec{v} \ . \ F$):
e, a = Solver(), Solver()
e.add($F$)
a.add($\neg F$)
$G$ = False
while sat == e.check():
$M_0$ = e.model()
$M_1$ = $\{ \mbox{literal }\ell \in F \;\mid\; M_0.\mathsf{eval}(\ell) = \true \}$  # assume $F$ is in negation normal form
assert unsat == a.check($M_1$)
$M_2$ = a.unsat_core()
$\pi$ = project($M_2$, $\vec{v}$)
$G$ = $G \vee \pi$
e.add($\neg\pi$)
return $G$


### From SMT to QBF and back

• The approach we illustrated was used by Monniaux'08 .

• QESTO  generalizes to nested QBF.

• We generalize QESTO to SMT; improving [25, 26, 31]

### Example game 

• : starts. .
• : strikes back. .
• : has to backtrack. Already .
• : learns .
• : .
• : counters - .
• : has lost!. Already .

### Summary of approach

• Two players try to find values

• - to satisfy
• - to satisfy
• Players control their variables

• at round :
• value of is already fixed,
• fixes value of ,
• fixes value of , but can change again it at round ,
• can guess values of of to satisfy .
• Some player loses at round .

• Create succinct no-good to strengthen resp. .

### Main ingredients: Projection and Strategies

• Projections are added to learn from mistakes.

• Player avoids repeating same losing moves.

• Strategies prune moves from opponent.

• Prevent opponent player from moves.

### Finding small good no-goods

• Player has lost at round

• Player found a model at round , .

• induces an evaluation on a subset of literals in , such that .

• is an unsatisfiable core for .

• Model Based Projection

• Find a , such that .

• should be weak, so is a strong blocker.
• should be cheap to find and avoid space overhead.
• Then can block .

• Idea: Use to find a sufficient .

### Initialization

   def level(j,a): return max level of bound variable in atom a of parity j     

### QSAT Algorithm

  def strategy(M,j): return $\bigwedge_{M \neq null, a \in Atoms, level(j, a) < j} sign(M,a)$
def tailv(j): return $x_{j-1},x_j,x_{j+1},\ldots$

j = 1
M = null
while True:
if $F_{j}\ \ \wedge$ strategy(M, j) is unsat:
if j == 1:
return F is unsat
if j == 2:
return F is sat
C = Core($F_j$, strategy(M, j))
J = Mbp(tailv(j), C)
j = index of max variable in J $\cup\ \{ 1, 2 \}$ of same parity as j
$F_j$ = $F_j \wedge \neg$J
M = null
else:
M = current model
j = j + 1


### Projection and Strategies

• Projections learn from mistakes, avoids similar mistakes in future rounds.

• Strategies prune moves from opponent.

### Model-based projection - Example

• Want to compute small .

• Note

• Say

• So

### Model-based Projection for LRA

Eliminate from conjunction of literals :

Trick: Use to turn into .

### Model-based Projection for LRA - resolution

Can now assume occurs only as upper or lower bounds:

### Model-based Projection on formulas

   def sign(M,a): if M(a) return a else return $\neg$a

### Model-based Projection for LIA

For LIA, cannot just assume equalities are of the form or . Generally, has a coefficient, that we cannot remove.

Example: .

• What could go wrong if we just reduce to ?

• Suppose , . So .

• Cross-multiplying gives , which is feasible, but is infeasible.

### Model-based Projection for LIA - integer resolution

Solution: Combine inequalities using resolution

### Model-based Projection for LIA - resolution 

•   if

• else if

• otherwise,

• satisfies , and

### Model-based Projection for LIA - divisiblity

Resolution introduced divisibility constraints.

So now we also have to eliminate under divisions.

where

• ,

### Model-based Projection for Term Algebras

S-expressions: A generic term algebra

• An s-expression is either a nil or a cons.

• Access arguments of cons using car and cdr.

• Test terms using cons?(), or nil?()

### Model-based Projection for Term Algebras - $\simeq$

amounts to unification

### Model-based Projection for Term Algebras - $\not\simeq$

Case for is symmetric.

Since there is an infinite number of cons-terms.

### Model-based projection Term Algebras - adequacy

• New terms are created during

• but they are of the form following shape of original constructor terms.

• and they occur in conjunctions with .

• so produces finite set of projections.

### Model-based projection for NRA

• Theory: Non-linear polynomial arithmetic

• Partial CAD - model-based projection 

• Given model , such that
• Find , such that
• is valid
• CAD decomposes into sign-invariant cylinders.

• Choose the cylinder where is a member.

### Model-based projections, two lenses

Sat based MBP :

• Given:

• Find: , free for

• Such that:

Contrast this with Core-based MBP :

• Given: .

• Find: , free for

• Such that:

Claim: (Roughly) The same projection operator can be used in both cases if occurs in all literals and the operator is stable under changes to the value of .

### Finding strategies

• Other main ingredient of QSAT is option for players to narrow options of opponents by revealing a strategy

• at round :
• value of is already fixed,
• fixes value of ,
• can make a function of .
• Developing practical strategies is work in progress

• For QBF can use Q-resolution proofs as guide 

• Method by Markus Rabe can be seen as a strategy.

## Horn Clauses [12–14, 24]

 def mc(x): if x > 100: return x - 10 else: return mc(mc(x + 11)) def contract(x): assert(x > 101 or mc(x) == 91)   (set-logic HORN) (declare-fun mc (Int Int) Bool) (assert (forall ((x Int)) (=> (> x 100) (mc x (- x 10))))) (assert (forall ((x Int) (y Int) (z Int)) (=> (and (<= x 100) (mc (+ x 11) y) (mc y z)) (mc x z)))) (assert (forall ((x Int) (y Int)) (=> (and (<= x 101) (mc x y)) (= y 91)))) (check-sat) (get-model)

### Horn Clause Engines

• PDR, SPACER - IC3 inspired engine [13, 23].
• Duality - Interpolation based .
• Use Duality, PDR, or SPACER if your Horn clauses use arithmetic variables.
• Datalog - Bottom-up stratified Datalog engine for finite domains .
• Use Datalog backened for Horn clauses over finite domains: bit-vectors and Booleans.
• BMC - Bounded model checking, Tabulation, Symbolic Execution
• Use BMC to unfold Horn clauses a la bounded model checking.

### IC3

• are state variables.

• is a monome (a conjunction of literals).

• is a clause (a disjunction of literals).

• Convention: is a monome over variables , is a renaming of the same monome to variables .

### IC3 recap

• - a transition system.
• - good states.
• - forward predicate transformer.
• Given reachable states , produce “states can be reached by including another step”.
• From Transition System:
• From Horn Clauses: , where

### IC3 recap (2)

• properties of states reachable within steps.
• are sets of clauses.
• Initially .
• a queue of counter-example trace properties. Initially .
• a level indication. Initially .

### Expanding Traces

repeat until

• Candidate If for some , , then add to .

• Unfold If , then set .

### Termination

repeat until

• Unreachable For , if , return Unreachable.

• Reachable If , return Reachable.

### Backtracking

repeat until

• Conflict Let : given a candidate model and clause , such that

• ,
• ,
then conjoin to , for .

• Leaf If , and is unsatisfiable, then add to .

### Inductive Generalization

repeat until

• Induction For , a clause , , if , then conjoin to , for each .

### Decide - Generalized form

Decide Add to if , .

• [6, 10] Model from propositional SAT check for gives (near prime implicant) .
•  Model from SMT check for arithmetical produces numerical assignment .
• [8, 21] Partial quantifier elimination.
•  where are quantifier-free. Use model for to compute without expanding full disjunction.
• [9, 15] Keep vocabulary of literals fixed (= predicate abstraction).

• Madoko is a A Fast Scholarly Markdown Processor,
• intuitive and powerful integration of markdown and LaTeX,
• browser and Azure based - no installation,
• immediate preview,
• real-time collaborative editing,
• is written in Koka,
• is by Daan Leijen, Microsoft Research ## References

Nikolaj Bjørner. “Linear Quantifier-Elimination as an Abstract Decision Procedure.” In IJCAR. 2010. 🔎
Nikolaj Bjørner, and Mikolás Janota. “Playing with Alternating Quantifier Satisfaction.” In LPAR Short Presentation Papers. 2015. 🔎
Nikolaj Bjørner, Mikolás Janota, and William Klieber. “On Conflicts and Strategies in QBF.” In 20th International Conferences on Logic for Programming, Artificial   Intelligence and Reasoning - Short Presentations, LPAR 2015, Suva, Fiji, November 24-28, 2015., 28–41. 2015. http://​www.​easychair.​org/​publications/​paper/​On_​Conflicts_​and_​Strategies_​in_​QBF🔎
Nikolaj Bjørner, Kenneth L. McMillan, and Andrey Rybalchenko. “On Solving Universally Quantified Horn Clauses.” In SAS, 105–125. 2013. 🔎
Maria Paola Bonacina, Christopher Lynch, and Leonardo Mendonça de Moura. “On Deciding Satisfiability by Theorem Proving with Speculative   Inferences.” J. Autom. Reasoning 47 (2): 161–189. 2011. 🔎
Aaron R. Bradley. “SAT-Based Model Checking without Unrolling.” In VMCAI, 70–87. 2011. 🔎
Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. “What’s Decidable About Arrays?” In Verification, Model Checking, and Abstract Interpretation, 7th International   Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings, 427–442. 2006. doi:10.1007/11609773_28🔎
Alessandro Cimatti, and Alberto Griggio. “Software Model Checking via IC3.” In CAV, 277–293. 2012. 🔎
Alessandro Cimatti, Alberto Griggio, Sergio Mover, and Stefano Tonetta. “IC3 Modulo Theories via Implicit Predicate Abstraction.” In TACAS, 46–61. 2014. 🔎
Niklas Eén, Alan Mishchenko, and Robert K. Brayton. “Efficient Implementation of Property Directed Reachability.” In FMCAD, 125–134. 2011. 🔎
Yeting Ge, and Leonardo Mendonça de Moura. “Complete Instantiation for Quantified Formulas in Satisfiabiliby   Modulo Theories.” In CAV, 306–320. 2009. 🔎
Sergey Grebenshchikov, Nuno P. Lopes, Corneliu Popeea, and Andrey Rybalchenko. “Synthesizing Software Verifiers from Proof Rules.” In ACM SIGPLAN Conference on Programming Language Design and Implementation,   PLDI ’12, Beijing, China - June 11 - 16, 2012, 405–416. 2012. doi:10.1145/2254064.2254112🔎
Krystof Hoder, and Nikolaj Bjørner. “Generalized Property Directed Reachability.” In Theory and Applications of Satisfiability Testing - SAT 2012 - 15th   International Conference, Trento, Italy, June 17-20, 2012. Proceedings, 157–171. 2012. doi:10.1007/978-3-642-31612-8_13🔎
Krystof Hoder, Nikolaj Bjørner, and Leonardo Mendonça de Moura. “μZ- An Efficient Engine for Fixed Points with Constraints.” In Computer Aided Verification - 23rd International Conference, CAV   2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, 457–462. 2011. doi:10.1007/978-3-642-22110-1_36🔎
Shachar Itzhaky, Nikolaj Bjørner, Thomas W. Reps, Mooly Sagiv, and Aditya V. Thakur. “Property-Directed Shape Analysis.” In CAV, 35–51. 2014. 🔎
Mikolás Janota, and Joao Marques-Silva. “Solving QBF by Clause Selection.” In Proceedings of the Twenty-Fourth International Joint Conference on   Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015, 325–331. 2015. http://​ijcai.​org/​Abstract/​15/​052🔎
Ajith K. John, and Supratik Chakraborty. “A Quantifier Elimination Algorithm for Linear Modular Equations and   Disequations.” In Computer Aided Verification - 23rd International Conference, CAV   2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, 486–503. 2011. doi:10.1007/978-3-642-22110-1_39🔎
Ajith K. John, and Supratik Chakraborty. “Extending Quantifier Elimination to Linear Inequalities on Bit-Vectors.” In Tools and Algorithms for the Construction and Analysis of Systems   - 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, 78–92. 2013. doi:10.1007/978-3-642-36742-7_6🔎
Ajith K. John, and Supratik Chakraborty. “A Layered Algorithm for Quantifier Elimination from Linear Modular   Constraints.” Formal Methods in System Design 49 (3): 272–323. 2016. doi:10.1007/s10703-016-0260-9🔎
Dejan Jovanovic, and Leonardo Mendonça de Moura. “Solving Non-Linear Arithmetic.” In Automated Reasoning - 6th International Joint Conference, IJCAR   2012, Manchester, UK, June 26-29, 2012. Proceedings, 339–354. 2012. doi:10.1007/978-3-642-31365-3_27🔎
Roland Kindermann, Tommi A. Junttila, and Ilkka Niemelä “SMT-Based Induction Methods for Timed Systems.” In FORMATS, 171–187. 2012. 🔎
Anvesh Komuravelli, Arie Gurfinkel, and Sagar Chaki. “SMT-Based Model Checking for Recursive Programs.” In CAV, 17–34. 2014. 🔎
Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki, and Edmund M. Clarke. “Automatic Abstraction in SMT-Based Unbounded Software Model   Checking.” In CAV, 846–862. 2013. 🔎
Kenneth L. McMillan. “Lazy Annotation Revisited.” In Computer Aided Verification - 26th International Conference, CAV   2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, 243–259. 2014. doi:10.1007/978-3-319-08867-9_16🔎
David Monniaux. “A Quantifier Elimination Algorithm for Linear Real Arithmetic.” In LPAR (Logic for Programming Artificial Intelligence and Reasoning), 243–257. Lecture Notes in Computer Science 5330. Springer Verlag. 2008. doi:10.1007/978-3-540-89439-1_18🔎
David Monniaux. “Quantifier Elimination by Lazy Model Enumeration.” In Computer-Aided Verification (CAV), 585–599. Lecture Notes in Computer Science 6174. Springer Verlag. 2010. doi:10.1007/978-3-642-14295-6_51🔎
Leonardo Mendonça de Moura, and Nikolaj Bjørner. “Efficient E-Matching for SMT Solvers.” In CADE, 183–198. 2007. 🔎
Leonardo Mendonça de Moura, and Nikolaj Bjørner. “Engineering DPLL(T) + Saturation.” In IJCAR, 475–490. 2008. 🔎
Leonardo Mendonça de Moura, and Nikolaj Bjørner. “Bugs, Moles and Skeletons: Symbolic Reasoning for Software   Development.” In IJCAR, 400–411. 2010. 🔎
Leonardo Mendonça de Moura, and Dejan Jovanovic. “A Model-Constructing Satisfiability Calculus.” In Verification, Model Checking, and Abstract Interpretation, 14th International   Conference, VMCAI 2013, Rome, Italy, January 20-22, 2013. Proceedings, 1–12. 2013. doi:10.1007/978-3-642-35873-9_1🔎
Anh-Dung Phan, Nikolaj Bjørner, and David Monniaux. “Anatomy of Alternating Quantifier Satisfiability (Work in   Progress).” In SMT-IJCAR, 120–130. 2012. 🔎
Ruzica Piskac, Leonardo Mendonça de Moura, and Nikolaj Bjørner. “Deciding Effectively Propositional Logic Using DPLL and   Substitution Sets.” J. Autom. Reasoning 44 (4): 401–424. 2010. 🔎
William Pugh. “The Omega Test: A Fast and Practical Integer Programming Algorithm   for Dependence Analysis.” In Proceedings Supercomputing ’91, Albuquerque, NM, USA, November 18-22,   1991, 4–13. 1991. doi:10.1145/125826.125848🔎
Andrew Reynolds, Tim King, and Viktor Kuncak. “Solving Quantified Linear Arithmetic by Counterexample-Guided Instantiation.” Formal Methods in System Design 51 (3): 500–532. 2017. doi:10.1007/s10703-017-0290-y🔎
Martina Seidl, Florian Lonsing, and Armin Biere. “qbf2epr: A Tool for Generating EPR Formulas from QBF.” In Third Workshop on Practical Aspects of Automated Reasoning, PAAR-2012,   Manchester, UK, June 30 - July 1, 2012, 139–148. 2012. http://​www.​easychair.​org/​publications/​paper/​145184🔎
Christoph M. Wintersteiger, Youssef Hamadi, and Leonardo Mendonça de Moura. “Efficiently Solving Quantified Bit-Vector Formulas.” Formal Methods in System Design 42 (1): 3–23. 2013. 🔎