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.