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.