HW 4: Analysis using Constraints

1. Read through paper:

• Program Analysis as Constraint Solving (Gulwani et al. 2008)
  • Focused only on Program Verification section

2. Hand-constraint solving on given example:

A bit of a replication of what's in the paper and what we went over in class however I needed additional work in understanding what exactly was going on.

1. Identification of constraints on our invariant I.
2. Application of an invariant template: a1x + a2y + a3 ≥ 0 ∨ a4x + a5y + a6 ≥ 0
3. Prep for Farkas' Lemma
4. TODO - Apply Farkas' Lemma (Briefly kicked around some ideas for "automatically" doing these things however decided I wanted to try something more concrete)

3. Install z3 and play around with toy examples

Install z3, peruse the documentation and a couple of quick guides, and run some toy examples. See example files:

• One trivially solved equation
• One unsatisfiable equation
• A couple of tests on basic laws or boolean algebra
• Example from Gulwani paper (after using invariant template and applying Farkas' Lemma to the first constraint)