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".