Good Music for Background

Dj Dave Liang, Miss Shanghai

Willing To See Real-World Formal Verification Tools

1. Why Project:    http://why.lri.fr/

    A general purpose Verification Condition Generator.

2. Pylint: http://www.logilab.org/857

    Static Checker for Python programs.

3. Code Analyzer for Visual Studio 2012

Question Regarding Groebner Basis

1. Can an ideal other than \( \{0\} \) be a finite set?

Answer: Yes. It's obvious to prove this conclusion.

2. What is monomial ideal?

Test SyntaxHightlighter on My Blogger

It works!

Improvement on Octogonal Method

In Deepak's method[1], when there is some constraint present at the verification condition (VC) generating position, the algorithm takes that constraint into consideration eagerly. This may result in a problem that the constraint might not be hit, like an infinite loop for instance. However, this constraint still enlarges the feasible domain of the octagon, which makes the generated VC weaker than the optimal one.

In order to address this problem, I make such a consideration lazy, which means that first apply the quantifier elimination method without constraints, and then compare the result with the constraints. Let U be the generated VC without constraints, and  P be the set of constraints (it can be test conditions or conditionals), if we can achieve that
                              \[ U \rightarrow P. \]
Then we can know that P will not be hit, which implies that we can ignore these constraints and U is right the final VC we want.

The original method is in P. If we consider to apply the two possible branches, i.e. either involve the constraints or not, at each position, then the method will be exponential. With my improvement, it's still exponential in worst case. But if I'm able to reduce the process of add constraints P back into U if necessary in constant time, then we can achieve an algorithm which can generate stronger program invariants but still in polynomial time.


---------------------------------
References:

[1] Kapur, Deepak, et al. "Geometric Quantifier Elimination Heuristics for Automatically Generating Octagonal and Max-plus Invariants." Automated Reasoning and Mathematics. Springer Berlin Heidelberg, 2013. 189-228.

Thoughts on Program Verification

Inspiration:
    I just finished the programming assignment in HW3 of Pattern Recognition class. There was a significant bug in my implementation on calculating the log-likelihood of the 1D Triangle Distribution, which resulted in the divergence of the parameter estimation.
    So I'm wondering whether it's feasible to maintain the correctness even for such data science programs (or scientific simulation in another perspective). In this domain, the key challenge is that the reason for such divergence can be either a bug or the usage of a wrong statistics model. In the latter case, this result cannot be called an error of the programs.
    Thus, my focus is on how to distinguish these two cases. If we are able to achieve this goal, it will be fairly convenient to debug the programs without doubting my choice of models, or on the other hand, I will only think about the pros and cons of the model itself with no concern about some potential bugs in the implementation.

Thoughts about Final Project in AdvHaskell

1. Implement abstract interpretation libraries in Haskell.

   a. There is one binding for PPL library in Haskell:
          http://www.ncc.up.pt/~pbv/research/ppl/ghc.html

   b. I would like to see whether Libapron and the tropical polyhedron library can be possible to implemented in Haskell.

   c. Importance: making Haskell eligible to do numerical static analysis for those compilers written in Haskell.

   d. Compiler.HOOPL package


2. Coq extraction to Haskell.

   a. A way to writing certified Haskell programs.

   b. Whether it's possible to hack in the Extraction component in Coq.

   c. comparing Haskell with Ocaml on coping with Coq Extraction.

   d. Adam Chlipala talks about some concepts about Generic Programming concerning Coq and Haskell:
                http://adam.chlipala.net/cpdt/html/Generic.html
          which might be helpful.

   e. This blog post talks about the Maybe monad emulated with properties proved in Coq:
               http://pdp7.org/blog/?p=100

Mar 13th, Meeting with Darko

1. Shall look up language extensions provided by GHC to address the following problem:

f :: (Eq a, Eq c) => (a -> a & c -> c) -> a -> c -> (a, c)
f g x y = (g x, g y)

g :: (Eq a) => a -> a
g x = x

main = do
    putStrLn $ show $ f g 3 'c'



2. Read the chapter about Univeral Types in TAPL book in order to understand forall tag for type variables in Haskell.

3. Look up semantics on concurrent programs to prepare for the next meeting with Darko.

Tiny Basic Interpreter Working Flow

1. Restructure Interpreter with two parts: 

     a)  Execute the program already stored on the code stack;

     b)  Evaluate the statement input from the Interpreter.

2. Finish the processing rule for INPUT statement.

3. Implement the RUN statement. (Maybe using CEK machine model)

4. Extend the language feature with:

     a)  RUN expr-list

     b)  LIST expr-list

Thoughts about Programming Language Implementation

1. An IDE that distinguishes variables regarding the scopes in which they are defined. This is particularly helpful for functional programs. The idea emerged from one Google Tech Talk on Monads and Gonads.

Better Than Simplex

I. Interior Point Method (by John von Neumann)

II. Ellipsoid Method (by Naum Z. Shor in 1972)

III. Karmarkar's Algorithm (by Narendra Karmarkar in 1984)

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?