Theory Solvers

Overview
Z3
MiniSAT
ZChaff variants

Overview

Our approach to program analysis, as validated in VS3, relies heavily on the use of efficient SAT and SMT solvers. The techniques we have developed maintain a distinct separation between the two phases of constraint generation and constraint solving. The constraint generation phase is oblivious of the underlying solver technology. Consequently, improvements in solver technology translate directly to a more efficient program analyses.

There are two motivations for experimenting with different solvers. First, performance considerations dictate that we find the solver that is most efficient. Second, we wish to evaluate if the specific form of the constraints that we generate from program analyses are amenable to specialized solving techniques. To date, we have identified some bottlenecks in solving (e.g. symmetry in constraints when invariants are disjunctive) but have not felt the need to modify any solvers.

On this page, we document our experience with different solvers. The attempt is to capture possible quirks that need not be re-discovered by others.

Z3

Our solver of choice is Z3--an experimental SMT solver from Microsoft Research. The notes here are by no means documentation for Z3. That can be found on the official Z3 documentation page. The objective is to tabulate general notes and this information is only provided as is.

Creating a context

A context for Z3 is created using the following sample code:

      Config c = new Config();
      c.SetParamValue("MODEL", "true");
      c.SetParamValue("QUANT_BOUND_INST", "true");
      p.SetParamValue("PARTIAL_MODELS", "true");  
      Context context = new Context(c);
      context.TraceToFile("tracefile.log");       
      context.Log("logfile.log");                  
      c.Dispose();

You can push context.Push() and pop context.Pop(optional num) context's so as to create traceback points. These are useful to clean the slate of any asserted facts and also when you want to try a set of extra assertions over a base.

Debugging

Logging and Assertion Traces
- Trace file: context.TraceToFile(filename) immediately after you create the context.
- Log file: context.Log(filename) immediately after you create the context.
If an implication evaluates to false then there is a way to get more insight into the problem. Create an SMT file with the constraint and get Z3 to generate a model for it. The model will be generated iff there is a satisfying assignment (i.e. antecedent and !consequent is satisfiable, meaning that the implication does not hold. The model is a witness).

Asserting quantified facts

Patterns in MkForall need a lot of explanation. We talk about important issues:

Cannot use interpreted functions in patterns:
Z3 does not support patterns with interpreted functions. For example "≤" and "+" are both interpreted--relation and arithmetic operators. On the other hand, nothing special needs to be done for select/store, only for arithmetic, relations and bit-vectors. There is a standard trick to avoid the interpreted function symbols in patterns, but still have the benefit of matching with them: For every interpreted function symbol add a ghost function. For example, for ≤ add the function my_LEQ Add axioms for them:
(forall (x y) { (my_LEQ x y) } (iff (my_LEQ x y) (<= x y)))
Use the ghost functions everywhere else, in patterns and in assertions that you need the relation, arithmetic and bit-vectors in.
Sorin Lerner's lecture slides have good intro to E-Matching and why triggers are important. In particular why it is important for the pattern/trigger to contain all quantified variables. The matching heuristic is intended to help the prover to quantify the variables. Therefore if some quantifier binders are left out then the matching will not result in a complete instantiation (which might, in some cases, be ok). The slides also contain an overview of combining decision procedures (Nelson-Oppen).

More to come!

MiniSAT

More to come!

ZChaff Variants

More to come!

Examples + Invariants Generated

Always under construction!

Overview
Invariants with Quantifiers
Invariants without Quantification
- Verification:
  - Disjunctive Invariant
  - Interprocedural Analysis
- Weakest Precondition Inference
- Strongest Postcondition Inference
- Applications:

Overview

On this page we present some illustrative examples to which a constraint-based program analysis can be applied. The examples have been purposely simplified to focus on the diversity of a constraint-based approach.

For each program analysis, we present one example. The code for the function is presented on the right and the invariants generated are presented on the left. The objective of this tabulation is a high-level summarization and the details of each sample program and analysis can be found in the appropriate papers.

Invariants with quantifiers

... To come.

Invariants without quantification

DisjLoop: [Inferring disjunctive invariants]
(x< 0 ∨ y> 0) →	x := 50; while (x < 0) { x := x + y; y++; } assert(y > 0)
McCarthy91: [Inter-procedural analysis]
(n > 100⇒ ret=n-10) ∧ (n ≤ 100⇒ ret=91) →	main() { result := call(19)+call(119); assert(result = 200); } call(int n) { if(n > 100) return n - 10; else return call(call(n + 11)); }
Array Copy: [Weakest Precondition]
(m1=0∧m2=0)∨(m3≥m1+m2) → → →	assert (m1,m2 ≥ 0); k := i := 0; while (i<m1) { assert (0≤k< m3); A[k++] := B[i++]; } i := 0; while (i< m2) { assert (0≤k< m3); A[k++] := B[i++]; }
Speedometer: [Strongest Postcondition]
true → (s+d+t≥ 0) ∧ (d≤ s+5t) →	d := t := s := 0; while (true) { if () t++; s := 0; else if () if (s < 5) d++; s++; }
FiniteIncrement: [Termination Analysis]
n≥ m+1 →	x := x0; y := y0; while (x < y) { x := x + n; y := y + m; }
Count to ∞: [Non-Termination Analysis]
x ≥ 0 ∧ y ≥ 0 →	while (x ≥ 0) { x := x + y; y++; }
HiddenBug: ["Weakest" Bug-Finding]
(n> 200)∧(0<y<9) →	x := 0; if (y < 9) { while (x < n) { assert (x < 200) x := x + y; } } else { while (x ≥ 0) { x++; } }

VS³: Verification and Synthesis using SMT Solvers

Overview

Personnel

Publications

The VS³ Tool

Overview

Download

Theory Solvers

Table of Contents

Overview

Z3

Creating a context

Debugging

Asserting quantified facts

MiniSAT

ZChaff Variants

Talks/Presentations

Examples + Invariants Generated

Table of Contents

Overview

Invariants with quantifiers

Invariants without quantification

VS3: Verification and Synthesis using SMT Solvers

Overview

Personnel

Publications

The VS3 Tool

Overview

Download

Theory Solvers

Table of Contents

Overview

Z3

Creating a context

Debugging

Asserting quantified facts

MiniSAT

ZChaff Variants

Talks/Presentations

Examples + Invariants Generated

Table of Contents

Overview

Invariants with quantifiers

Invariants without quantification

VS³: Verification and Synthesis using SMT Solvers

The VS³ Tool