Revisions to loops paper.
extend to parallel programs.
(even just simple case of loop with barrier)
related work:
Abadi & Lamport [ACM Theor. Comp. Sci. 1991]
Sketching Stencils Armando Solar-Lezama, Gilad Arnold, Liviu Tancau, Rastislav Bodik, Vijay Saraswat and Sanjit Seshia ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'07) San Diego, CA, June 2007
Control-Flow Refinement and Progress Invariants for Bound Analysis, PLDI 2009, Sumit Gulwani, Sagar Jain, and Eric Koskinen
other tools: Klee, find all the other tools that do some kind of loop equivalence checking, try to run them on our examples, compare with ours.
find a better way to define the method
walk step by step through the algorithm
better examples. Not these little trivial things.
stressing of the technique: how big can you scale, limitations
example where bug can be found that cannot be found with bounded approach (grading example)
find at least some of the invariants automatically
