Formal Verification: Lab exercises with CBMC

CBMC resources

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


    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


    ./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

Home : Teaching : Courses : Fv 

Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland, UK
Tel: +44 131 651 5661, Fax: +44 131 651 1426, E-mail:
Please contact our webadmin with any comments or corrections. Logging and Cookies
Unless explicitly stated otherwise, all material is copyright © The University of Edinburgh