1. things to do for CIVL:
 - report file not found nicer
 - report concrete # procs in message passing required nicer
 - check args to int div/mod nonnegative
 - check out other uses of "bundle"
 - maybe record a video for CIVL tutorial?

2. SARL: do what Green does:
  - slice
  - persistent storage of cache
  - renaming the variables
  - Z3?

3. Make it easy to specify a dependence relation with a library. Use this in POR. Example: send and recv are independent (usually).

4. Add scope parameter to $heap?  meaning: pointers in this heap never leave scope

5. Add visitor pattern to model?

6. No static escape analysis needed -- use dynamic escape analysis, read Matt's FMSD paper

7. Consider implementing a fence or barrier or other structures as primitives

8. Examples
 - Get examples from [wiki:Examples], compile
 - Translate benchmarks from CVT/TASS to CIVL
 - Create a SVN repository for examples (both original code and translation in CIVL)

9. Find other tools to compare with CIVL
  - e.g. CBMC, DIVINE