GNU 30th Anniversary

 

GNU is 30 years old now!

Review on Decision Procedure on Linear Arithmetic

This is about the review of topics that De Moura covered in SSFT2013.

1. Here is my implementation on Sturm's Theorem in Univariate Polynomial case:

https://github.com/yihming/algebraic_geometry

    The language I choose is Haskell.

2. Here is my proof of Sturm's Theorem:

Day V: Summer School on Formal Techniques

Putting Numerical Abstract Domain to Work: A Study of Array-Bound Checking for C Programs (by Arnaud J. Venet, slides):

    1. Review of Abstract Interpretation using Polyhedra abstract domain;
          My Question: what is the difference between polyhedron intersecting and the narrowing operator?
    2. Gauge domain: modified interval domain to help scale the operations within loops (specifically, widening and convex-hull operations);
    3. He uses New Polka library and XXX's fixed-point algorithm:
        a. Issue: Program Crashed for widening operations: too many dimensions (i.e. program variables). Solution: eliminate unimportant variables;
        b. Issue: still crashed. Solution: directly propagate unchanged constraints rather than calculate again and again. Solved.


Verified Programming in VCC (by Ernie Cohen, slides):

    1. VCC is heavily based on ghost data, which costs zero executing time;
    2. There is no invariant check when VCC applies the owning operation on objects;
    3. Verification on concurrent programs: lock-free; lock is container.

Program Verification and Synthesis as Horn-like Constraint Solving (by Andrey Rybalchenko):

    1. verification using temporal logic (especially CTL);
    2. Doing abstract interpretation using horn-like constraint solving strategy (using Interpolant).

Lab (by Ernie Cohen):
    1. Write you own binary search program in C;
    2. Use VCC (either in Visual Studio or with online version (http://rise4fun.com/Vcc)) to verify the code;
    3. VCC code you need to write: function-level (pre-condition using requires; post-condition using ensures; terminating using decreases), loop-level (invariant specification).
    4. My original code has 27 bugs, all of which are related to overflow. After fixing it for one hour, I get it bug-free under VCC verification.

Day IV: Summer School on Formal Techniques

Automatic Deduction Applied: Program Synthesis and Question Answering (by Richard Waldinger, slides):
    1. Program Synthesis: extracting programs from proofs;
    2. History on Automatic Deduction:
         a. McCarthy's advice taker;
         b. Slagle's deducum;
         c. Amphion system used in planetary astronomy;
    3. Question in natural language and based on deduction rather than statistical search (on which IBM Watson applies)

Program Verification and Synthesis as Horn-like Constraint Solving (by Andrey Rybalchenko, slides):
    1. Summarization vs. Invariance :
         a. For the case with procedure invocations;
         b. Owicki / Gries Proof Rule;
         c. Rely / Guarantee Proof Rule;
     2. Type System in Programming Languages:
         a. Well-typed programs can never go wrong;
         b. Type Tree vs. Refinement Tree (PVS-friendly specification).
       Exercise proposed by Shankar: use PVS to write the specification for 2b, and submit to him.

Static and Dynamic Analysis of Concurrent Programs (by Aarti Gupta, slides):
    1. Context Bounded Analysis using Sequentialization;
    2. Dynamic Analysis:
          a. Preemptive Context Bounding;
          b. Trace Based Verification;
          c. Predicative Analysis;
    3. Garbage Collection in C++11;
    4. SMT-Based symbolic search:
          a. based on Concurrent Static Single Assignment (CSSA) encoding;
          b. Modular Analysis.

Lab (by Andrey Rybalchenko):
      ARMC: http://www7.in.tum.de/~rybal/
  My Comment: it can be easily screwed up writing a much longer horn-like constraint verification code, even for just 20 lines of source code with inter-procedure calls. Is there any related work or possibility to generate these constraints automatically?
   Prof. from CAS commented: Horn Clause was under warm studying and researching during 1980s. Then people came to obstacles and put it on the shelf for a long time. Recently it returns to alive. Deepak has done a bunch of elegant stuffs, including Ideal Generation, etc.

PPT Karaoke for fun tonight.

Day III: Summer School on Formal Techniques

Speaking Logic (by N. Shankar, slides):
    1. Unification;
    2. Resolution (Negation -> Prenexation -> Skolemization -> Distribution and Isolation -> Universal Quantifier Elimination -> Q.E.D.)

Static and Dynamic Verification on Concurrent Programs (by Aarti Gupta, slides)

Verified Programming in VCC (by Ernie Cohen, slides):
    1. "Programming Pearls" Chapter -- How to verify Binary Search;
    2. Separation Logic;
    3. Positive Polarity;
    4. Linearly Isolability.

Lab (Aarti Gupta, instructions):

Active Testing: CalFuzzer  http://sp09.pbworks.com/w/page/6721195/FrontPage
                                       http://srl.cs.berkeley.edu/~ksen/calfuzzer/
Homework: http://sp09.pbworks.com/w/page/6721216/RaceFuzzer%20Homework


Student Presentation:
     1. Anvesh Komuravelli, "Abstraction in SMT-based Model Checking".
        a. Predicate Abstraction;
        b. SLAM, BLAST, SDV; IMPACT, UFO;
        c. Over-approximation Driven; Under-approximation Driven;
        d. His approach is a little bit like widening operator in Abstract Interpretation. The difference is that it can approximate with respect to the counterexample, which is the feature of Model Checking (Dynamic Analysis);
        e. Using UZ SMT Solver.

      2. Sridhar Duggirala, "Annotations for Verification of Dynamical and Hybrid Systems".

Day II: Summer School on Formal Techniques

Speaking Logic (by N. Shankar, slides):

    1. Sequant Calculus (contd.) -- Cut rule;
    2. Peirce's Formula: $$ ((p \Rightarrow q) \Rightarrow p) \Rightarrow p $$;
    3. Concepts of derivied rule and admissible rule;
    4. How to prove  $$\exists x. (p(x) \Rightarrow \forall y. p(y))$$;
    5. Prenex Normal Form.

PVS (by C. Munoz, lecture 2):

    1. Proof by Induction (proving strategy; can go around by making use of data type specifications);
    2. Recursion specification.

Decision Methods on Arithmetic (by L. de Moura, slides and materials):

    1. Multivariate case: recursive representation of multivariate polynomials (with some order on variables);
    2. Sturm Tree -- Case analysis based on Sturm's sequence and Tarski query;
    3. Leonardo's method is built in the Z3 theorem prover.

Discussion with Leonardo de Moura:

    For the proof of Sturm's Theorem, most proofs only consider the case that  \( h_m\)  is a constant polynomial. However, though rarely, there can be the case that   \( h_m \)  is a non-constant polynomial. In the latter case, we need to divide each polynomial in the Sturm Sequence by  \( h_m \)  and show that the resulting sequence  \( \hat{h_i} \) is still a sequence of polynomials. Further, to prove that the only point that decreases the total sign change number is the real root of \( f \), we need to discuss by case analysis on the sign of \( \hat{h_1} \) using the property of even and odd functions.

PVS Lab Session (instructions, homework):

    1. PVS examples in PVSLab directory provided by Munoz;
    2. PVS 6.0 with NASALib installed (http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/);
    3. discussion with students: the online textbook named "Software Foundations" by Benjamin C. Pierce (http://www.cis.upenn.edu/~bcpierce/sf/).

Student Presentation:

    1. Martin Schäf, Joogie: Infeasible Code Detection on Java bytecode. 
        a. https://code.google.com/p/joogie/ ;
        b. Uses Soot (Java Optimization Framework), Wala (static analyzer on Java and JavaScript), and Z3 Theorem Prover;
        c. Based on Weakest Liberal Precondition rather than Weakest Precondition, i.e. only consider partial correctness;
        d. Can outperform the static code checker in Eclipse;
        e. Can have issues on false positive cases;
        f. He is a postdoc at United Nations University -- International Institute for Software Technology at Macau, China.

    2. Etienne Kneuss, "Leon Verification and Synthesis":
        a. Using Scala;
        b. Writing specifications on data structures and functions, then the system will search in the library to synthesize the reified code;
        c. Purely functional style syntax defined by them;
        d. Issues: due to the functional syntax, many real-world data structures like Doubly-Linked List cannot be specified; besides, High-order is not possible to be combined in.

Day I: SRI Summer School on Formal Methods

Speaking Logic (by Natarajan Shankar, slides here):

    1. How logic formalization can be used to address ruddles;
    2. Couturant, "Algebra of Logic";
    3. Substitution Lemma in propositional logic;
    4. Sequant Calculus.

PVS (by Cesar Munoz, lecture 0, lecture 1):

    1. TCAS alerting logic;

Decision Methods for Arithmetic (by Leonardo de Moura, slides and materials):

    1. Fourier-Motzkin Elimination Method;
    2. Sturm's Sequence;
    3. Sturm-Tarski Theorem;
    4. Tarski Query;
    5. Formal statement in univariate case.

Lab Session on Arithmetic Decision Methods (assignment):
    1. Tutorials on Z3: http://z3.codeplex.com/documentation ;
                                   http://stackoverflow.com/users/2327608/juan-ospina?tab=questions&sort=activity ;

    2. Prove Sturm's Theorem;

    3. Implement polynomial operations (+, *, /, etc.); Implement Sturm Sequence generating method; implement Tarski Query.  Note: All only in univariate cases.


Student Talks:
    1. Konstantin Korovin, Nestan Tsiskaridze, and Andrei Voronkov, Conflict Resolution:
        a. Used for solving linear (in)equality systems [satisfiability] on integer, real and rational fields;
        b. Based on Fourier-Motzkin Elimination;
        c. Main Method: 1) Assignment Refinement; 2) Constraint Generation based on Conflict;
        d. Drastically reduce the number of redundant constraints generated, i.e. better than Fourier-Motzkin Elimination, comparable to Simplex Method;
        e. Heuristics on choosing conflicting constraints: mini-lower, max-upper; or longest geometric distance;
        f. Easy to switch to incremental version;
        g. Suitable for combining with SMT solver;
        h. Future Work: combine with SMT solver; implement a better preprocessor.

    2. Gidon Ernst, et al. "A Formal Model of a Virtual Filesystem Switch":
        a. https://swt.informatik.uni-augsburg.de/swt/projects/ ;
        b. Implement a simulation on the very top level, the core part (i.e. the part dealing with flash disks) is still under developing;
        c. Specification written in PVS, implementation in Scala.

AIHaskell: Final Project for CS 591

Part I. Front-end

   I choose Parsec library to help implement the front-end. A sample of its usage can be found here:

                    http://book.realworldhaskell.org/read/using-parsec.html

Dimension Analysis in multiple languages

http://meltumn.wordpress.com/2012/03/21/existing-approaches/

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?