Minimal Comprehensive Groebner Bases

Goals:

1. Decide if the transitivity of non-essentiality is necessary;
2. Prove the generated Groebner basis is minimal, faithful and comprehensive;
3. Extend it to general comprehensive Groebner systems;
4. Try to define the Canonical Minimal Comprehensive Groebner basis.


Done:

1. We do need the transitivity of non-essentiality to guarantee the comprehensiveness of the generated Groebner basis;

2. Faithfulness and comprehensiveness are trivial to prove; Minimality is able to be proved;

3. Extension: replace "LPP_X is x" by "LPP_X divides x".

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.