Meeting with Deepak

Tasks:

1. Whether interior-point algorithm can work on Max-Plus Polyhedra. Check the book Introduction to Algorithms.

2. Rodriguez-Carbonell's work on invariant generating. Exponential

3. Check the paper introducing Standard Polyhedra for how to generate the convex hull of two polyhedra.

4. For programs with multiple paths, one way to preventing exponential runtime invariant generating is to get the invariant for each conditional path, then combine them along the linear path. (2^k -> k) However, the generated invariant should be weaker than the one using the exponential algorithm. Evaluate how weak this invariant can be.

5. Read the book on Abstract Algebra. See whether I'm comfortable with this mathematical foundation.

6. For the method combining Octagon and Max-Plus Polyhedron, check whether some of the disjunction constraints can subsume others. If so, then by scanning all the generated constraints, we can eliminate some of them to simplify the work.

7. Check Miné's paper:  
          A. Miné. Weakly relational numerical abstract domains. These de doctorat en informatique, École polytechnique, Palaiseau, France, 2004.


------------ Deepak's Follow on --------------------------

If you recall we discussed in the class how abstract interpretation works. Mine's thesis is about using octagonal formulas as the abstract
domain for generating invariants using abstract interpretation.

An interesting thing worth study would be to analyze how Mine' ignores or incorporates the disjunctive behavior potentially arising from
the presence of tests/conditions. As you discussed, we ignore the literal corresponding to the absence of a test when the test
is present. Does that happen in abstract interpretation? I conjecture not, but then why does the abstract interpretation also come
up with a weak invariant?