Verification of C programs with VCC

• VCC website
• VCC online version
• VCC tutorial
• Data Abstractions in VCC (paper by Ernie Cohen)
• Floyd-Hoare logic
• How VCC works
• Annotations in VCC
• Sample programs
  • max3.c
  • fun.c
  • add.c
  • pointer.c
  • memcopy.c
  • arrayinit.c
  • linsearch.c
  • byte-counter.c
• Assignment 4
  The given implementation: overflow-delayed.c
  A possible solution: overflow-delayed-joint.c.