Verification of C programs with VCC

• VCC website
• Script to install VCC on Linux by Arnab Chatterjee, MTech 2020.
• VCC online version (defunct now)
• VCC tutorial
• Data Abstractions in VCC (paper by Ernie Cohen)
• Floyd-Hoare logic
• How VCC works
• Annotations in VCC
• Some examples done in class:
  • Basic VCC usage vcc-basic.c
  • Function contracts vcc-functions.c
  • Pointers vcc-pointers.c
  • Ghost types vcc-ghost.c
  • Checking refinement conditions: Queue example queue-joint.c