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.