University Homepage School Homepage School Contacts School Search

Formal Verification: Lab exercises with CBMC

CBMC resources

• CBMC Homepage.
• CPROVER Manual. This is the main documentation page on CBMC and related tools.
• Paper introducing CBMC
• Short tutorial on CBMC

Lab instructions

For this lab, follow the CBMC short tutorial which provides a hands-on introduction to the CBMC tool.

1. Download this file lab.tar to some directory in your DICE file-space and unpack it using the command

   tar xf lab.tar

   This will create a directory lab containing an executable file cbmc and the example C files

   file1.c
   file2.c
   binsearch.c
   lock-example.c
   lock-example-fixed.c

   used by the CBMC tutorial.

2. To run the executable, set lab as your current directory and type ./cbmc. E.g.

   ./cbmc file1.c --show-properties --bounds-check --pointer-check

   Type

   ./cbmc --help

   to see a full range of options accepted by CBMC.

3. When you get to the lock-example.c example, run CBMC generating a counter-example trace and note how the counter-example points to the problem with the code. See lock-example-fixed.c for a fixed version of the code.

---

Last modified: 11:00 Wed 29 Mar 2017