Applications of CBMC

The following papers describe interesting applications of CBMC:

Error explanation and localization

• Error Explanation with Distance Metrics
  This paper describes a modified version of CBMC that can find the cause of an error.
• Automated Fault Localization for C Programs
  CBMC is used to localize the possible cause of a fault.

Concurrency

• Bounded Model Checking of Concurrent Programs
  This paper describes a version of CBMC for concurrent software.

Equivalence Checking

• Partial Translation Verification for Untrusted Code-Generators
  CBMC is used for translation validation of Simulink and generated ANSI-C.
• Translation Validation: From Simulink to C
  An application of CBMC for translation validation of Simulink and generated ANSI-C.
• Inference rules for proving the equivalence of recursive procedures
  This paper describes an algorithm to show equivalence of two programs. The resulting verification condition is discharged with CBMC.
• An Efficient System-Level to RTL Verification Framework for Computation-Intensive Applications
  CBMC is used on various arithmetic circuit models.

Practical Applications and Experience Reports

• Model checking C source code for embedded systems
  This paper contains a cast stuidy in which CBMC is applied to software for the ATMEL ATmega16, a small embedded processor.
• Integrated Static Analysis for Linux Device Driver Verification
  This paper describes an application of CBMC to the verification of Linux Device Drivers.
• Academic tools and reallife bug finding in Win32
  This paper describes an application of CBMC to finding security-relevant bugs in WIN32 binaries.
• Reducing False Positives by Combining Abstract Interpretation and Bounded Model Checking
  An application of CBMC to filter warnings generated by PolySpace.
• Configuration Lifting: Verification meets Software Configuration
  CBMC is used to verify multiple configurations of a program simultaneously.
• Semiformal Verification of Embedded Software in Medical Devices Considering Stringent Hardware Constraints
  An application of CBMC and SATABS to a medical device.
• Formal Verification of a Flash Memory Device Driver – An Experience Report
  An application of CBMC (and other Model Checkers) to a device driver.
• Concolic Testing of the Multi-sector Read Operation for Flash Memory File System
  An evaluation of concolic testing on file system code.
• Unit Testing of Flash Memory Device Driver through a SAT-Based Model Checker
  An application of CBMC in unit testing.
• Cross-Platform Verification Framework for Embedded Systems
  CBMC is applied to software for Motorola's HCS12.
• SMT-Based Bounded Model Checking for Embedded ANSI-C Software
  CBMC generates VCCs for embedded software, which are passed to a collection of recent SMT solvers.
• Why does ASTRÉE scale up?
  The paper includes a comparison with CBMC.

Test-vector generation

• Automatic Test Generation for Coverage Analysis of ERTMS Software
  Automatic Test Generation for Coverage Analysis Using CBMC
  CBMC is used to generate tests for components of the European Railway Traffic Management System.
• Abstraction-guided Test Generation: A Case Study
  A Theory of Predicate-Complete Test Coverage and Generation
  These papers describe an application of CBMC to test-vector generation. There is also a patent on this.
• Query-Driven Program Testing
  An application of CBMC for test-vector generation.

Worst-case execution time

• Measurement-Based Timing Analysis
  An application of CBMC to WCET analysis.
• Using a Model Checker to Determine Worst-case Execution Time
  CBMC is used to determine the worst-case number of loop iterations.

We are happy to hear about applications of CBMC and your experience.