Applications of CBMC

The following papers describe interesting applications of CBMC.

Error explanation and localization

• VART: A Tool for the Automatic Detection of Regression Faults
  CBMC is used for regression verification.
• Regression aware debugging for mobile applications
  CBMC is used to debug mobile applications.
• 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.
• Automated Program Debugging via Multiple Predicate Switching
  An application of CBMC to fault localization.
• Cause Clue Clauses: Error Localization using Maximum Satisfiability
  CBMC is combined with a MAX-SAT solver to localize bugs in C programs.

Concurrency

• Simulating Operational Memory Models Using Off-the-Shelf Program Analysis Tools
  CBMC is used as an alternative to a simulator for axiomatic memory models, including an application to a memory model for programs that interact with an FPGA.
• The Semantics of Shared Memory in Intel CPU/FPGA Systems
  CBMC is used to check programs that interact with an FPGA.
• Bounded Model Checking of Concurrent Programs
  This paper describes a version of CBMC for concurrent software.
• Time-Bounded Analysis of Real-Time Systems
  CBMC is used to check software with periodic rate-monotonic scheduling.
• Compositional Sequentialization of Periodic Programs
  CBMC is used to check compositional sequentializations of periodic programs.
• Data Race Detection for Interrupt-Driven Programs via Bounded Model Checking
  CBMC is used to analyse a serialization of a concurrent interrupt driven program as a non-deterministic sequential program.
• CSeq: A Concurrency Pre-processor for Sequential C Verification Tools
  CBMC is used to check sequentializations of concurrent programs; the paper also includes a comparison with the partial-order based CBMC.
• Regression-free Synthesis for Concurrency
  CBMC is used to generate traces of concurrent programs for program repair.
• BBS: A Phase-Bounded Model Checker for Asynchronous Programs
  CBMC is used to check sequentialisations of C programs.

Equivalence Checking

• Registered Report: Generating Test Suites for GPU Instruction Sets through Mutation and Equivalence Checking
  CBMC is used to generate tests for checking the semantics of NVIDIA's PTX ISA given in C against an implementation.
• EPEX: Processor Verification by Equivalent Program Execution
  CBMC is used to translate a RISV-C ISA into SMT-LIB to generate equivalent program mutants.
• Partial Translation Verification for Untrusted Code-Generators
  CBMC is used for translation validation of Simulink and generated ANSI-C.
• Translation Validation for Stateflow to C
  CBMC is used 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.
• Equivalence Checking between Function Block Diagrams and C Programs Using HW-CBMC
  HW-CBMC is used to check equivalence of IEC 61131-3 PLC Function Block Diagrams and manually written C code. A short version is here.

Cyper-physical Systems and Control

• A Verified Low-Level Implementation of the Adaptive Exterior Light and Speed Control System
  CBMC is used to verify a MISRA-C implementation of the 2020 ABZ case study.
• Experience with Static PLC Code Analysis at CERN
  CBMC is used to verify PLC code.
• A Toolset for Validation and Verification of Automotive Control Software Using Formal Patterns
  CBMC is used to verify API usage rules in automotive OSEK/VDX applications.
• Automated Domain-Specific C Verification with mbeddr
  CBMC is used to verify embedded programs given in a domain-specific modeling language. The paper includes an example from the Pacemaker Challenge.
• Cyber/Physical Co-Verification for Developing Reliable Cyber-Physical Systems
  CBMC is used to verify a combination of a controller and a plant-model in the automotive domain.
• Runtime Verication for Ultra-Critical Systems
  Copilot uses CBMC to verify embedded C programs generated from a Haskell-based data-flow DSL.
• Linking Functional Requirements and Software Verification
  An application of CBMC to check functional requirements of automotive software.
• A Framework for Analysing Driver Interactions with Semi-Autonomous Vehicles
  CBMC is used to verify a combination of a model of human behavior with vehicle control software.
• Reachability Verification of Rhapsody Statecharts
  CBMC is applied to the verification of Rhapsody statecharts.
• Applying Software Model Checking to PALS Systems
  CBMC is applied to PALSWare and applications on top of PALSWare.

Further Practical Applications and Experience Reports

• A Verification Methodology for the Arm® Confidential Computing Architecture: From a Secure Specification to Safe Implementations
  CBMC is applied to a reference implementation of ARM's Realm Management Monitor
• Formal Verification of an Industrial Distributed Algorithm: An Experience Report
  CBMC is applied to a distributed algorithm at Thales
• Benchmarking Software Model Checkers on Automotive Code
  CBMC is applied to two R&D prototype Simulink models from Ford
• A Preliminary Study on Open-Source Memory Vulnerability Detectors
  The paper includes a broad comparison including memory safety dynamic checkers on a set of micro benchmarks.
• Taming Interrupts for Verifying Industrial Multifunction Vehicle Bus Controllers
  CBMC is used to check sequentializations of interrupt-driven code
• Automated Verification for Functional and Relational Properties of Voting Rules
  CBMC is used to analyze implementations of voting rules
• SAT-based Bounded Software Model Checking for Embedded Software: A Case Study
  CBMC is used to analyze ls in busybox, with a comparison with concolic testing
• Crowdsourcing Program Preconditions via a Classification Game
  CBMC is used to check candidate preconditions
• How Verified is My Code? Falsification-Driven Verification
  CBMC is used together with mutation analysis on the Read-Copy-Update (RCU) mechanism in the Linux kernel.
• CRUST: A Bounded Verifier for Rust
  CBMC is used to check memory safety of unsafe Rust code.
• Bridging the gap between test cases and requirements by abstract testing
  CBMC is used for abstract testing, with a a case study from the automotive systems domain.
• On the formal verification of component-based embedded operating systems
  CBMC is used for checking contracts for an embedded operating system scheduler written in C++.
• Comparing Model Checking and Static Program Analysis: A Case Study in Error Detection Approaches
  The paper contains a comparison of BMC and a static analyzer on a large collection of benchmark programs.
• Correctness of Sensor Network Applications by Software Bounded Model Checking
  The paper describes an automatic verification method for TinyOS software including a behavior model for a network protocol.
• Formal Verification of Software for the Contiki Operating System Considering Interrupts
  The paper describes an application of CBMC to the verification of interrupt-driven code running on Contiki nodes
• Software verification for TinyOS
  This is the first paper describing the verification of TinyOS 2, MSP430 applications. An extended variant is here.
• Model checking C source code for embedded systems
  This paper contains a case study 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.
• Reducing False Positives by Combining Abstract Interpretation and Bounded Model Checking
  An application of CBMC to filter warnings generated by PolySpace.
• Efficient Elimination of False Positives Using Bounded Model Checking
  The paper presents two novel techniques to speed up filtering of alarms generated by abstract interpretation.
• 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. The journal version is here.
• Unit Testing of Flash Memory Device Driver through a SAT-Based Model Checker
  An application of CBMC in unit testing.
• A Comparative Study of Software Model Checkers as Unit Testing Tools: An Industrial Case Study
  A comparison of CBMC and Blast on flash memory controller code.
• 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.
• Verifying Code and Its Optimizations: An Experience Report
  CBMC is used to verify a speed-optimized implementation of a CRC in an automotive setting.
• Property-based Code Slicing for Efficient Verification of OSEK/VDX Operating Systems
  CBMC is applied to sliced kernel code of the Trampoline OS.
• Assertion Checking Using Dynamic Inference
  CBMC is integrated into a refinement loop for summaries of code fragments. Daikon generates invariant candidates.

Test-vector generation

• Diversifying Focused Testing for Unit Testing
  CBMC is used to generate a set of diverse test inputs.
• Model-based testing of automotive software: some challenges and solutions
  CBMC is used for generating tests for an automotive application.
• Automatic Test Generation for Coverage Analysis of ERTMS Software
  Automatic Test Generation for Coverage Analysis Using CBMC
  Using Bounded Model Checking for Coverage Analysis of Safety-Critical Software in an Industrial Setting
  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.
• Masking Boundary Value Coverage: Effectiveness and Efficiency
  CBMC is used to generate test-vectors for a new coverage criterion called MBVC.
• Test Generation for Large Automotive Models
  CBMC is used to generate test-vectors for models from the automotive domain, with a focus on floating-point arithmetic.
• Combining Static Analysis and Constraint Solving for Automatic Test Case Generation
  The paper includes a comparison with KLEE and CBMC on string-buffer related benchmarks.
• Scaling Model Checking for Test Generation Using Dynamic Inference
  CBMC is used to check invariants generated by Daikon for the purpose of test generation.

Worst-case execution time

• Scalable and precise estimation and debugging of the worst-case execution time for analysis-friendly processors: a comeback of model checking
  CBMC is used for WCET analysis of programs for the Atmel AVR family.
• WCET Overapproximation for Software in the Context of a Cyber-Physical System
  CBMC is used to overapproximate the WCET of SPARC code in a CPS controller.
• Scalable and Precise Refinement of Cache Timing Analysis via Model Checking
  An application of CBMC to WCET with emphasis on cache performance.
• 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.
• Determining the Worst-Case Reaction Time of IEC 61499 Function Blocks
  CBMC is used to determine the worst-case reaction time of function blocks in IEC 61499 programs.
• Fully-automatic derivation of exact program-flow constraints for a tighter worst-case execution-time analysis
  CBMC is used to validate high-level WCET hypotheses derived from test runs.

Security

• Proving UNSAT in Zero Knowledge
  CBMC is used to generate encodings of C programs for zero-knowledge proofs of unsatisfiability
• Discovery and Identification of Memory Corruption Vulnerabilities on Bare-metal Embedded Devices
  CBMC is used in a setup for fuzzing IoT code
• Evaluating and comparing memory error vulnerability detectors
  The paper features a comparison of CBMC with dynamic checkers on a set of benchmarks for memory safety.
• Translation of Algorithmic Descriptions of Discrete Functions to SAT with Applications to Cryptanalysis Problems
  CBMC is applied to a wide range of cryptanalysis problems.
• Symbolic Verification of Cache Side-Channel Freedom
  CBMC is used in an abstraction-refinement loop to generate fixes for cache side channel vulnerabilities in C programs.
• An Algorithmic Approach to Formally Verify an ECC Library
  CBMC is used to verify the implementation of a library for elliptic curve cryptography.
• Practical Detection of Entropy Loss in Pseudo-Random Number Generators
  CBMC is used to detect weak random number sources. A CVE is here.
• Applied Quantitative Information Flow and Statistical Databases
  Quantifying Information Leaks in Software
  SAT-based Analysis and Quantification of Information Flow in Programs
  Abstract model counting: a novel approach for quantification of information leaks
  Quantifying Dynamic Leakage
  CBMC is used to measure information leakage in programs.
• Parametric Verification of Address Space Separation
  CBMC is used to check abstractions of the ShadowVisor and Xen hypervisors for security
• Design, Implementation and Verification of an eXtensible and Modular Hypervisor Framework
  CBMC is used to check the XMHF hypervisor
• Secure Two-Party Computations in ANSI C
  CBMC is used to produce circuits for Secure Two-Party Computation
• Finding Security Vulnerabilities in a Network Protocol Using Parameterized Systems
  CBMC is used to construct scenarios that permit attacks on OSPF
• Academic tools and reallife bug finding in Win32
  This paper describes an application of CBMC to finding security-relevant bugs in WIN32 binaries.
• Verifying security patches
  The paper uses CBMC to compare a patched version of a program to the original.

Java

• Proving JDK's Dual Pivot Quicksort Correct
  CBMC is used to discharge hard VCCs in a proof of JDK's sorting.

Others

• C Description Reconstruction Method from a Revised Netlist for ECO Support
  CBMC is used in a CEGIS loop to synthesise expressions to recreate a high-level model of a modified netlist
• Discovering vesicle traffic network constraints by model checking
  CBMC is used to discover Rothman-Schekman-Sudhof molecular transport topologies within eukaryotic cells
• Equivalence Checking on ESL Utilizing A Priori Knowledge
  CBMC is used within an IC3 implementation for hardware equivalence checking
• Proving Transaction and System-level Properties of Untimed SystemC TLM Designs
  An application of CBMC to C programs extracted from SystemC TLM models
• Induction-Based Formal Verification of SystemC TLM Designs
  CBMC is used to verify SystemC TLM models
• Robustness Analysis of Floating-Point Programs by Self-Composition
  CBMC is used for robusness analysis of floating-point code
• Incremental test case generation using bounded model checking: an application to automatic rating
  CBMC is used to rate solutions to programming exercises

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