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.