Applications of CBMC
The following papers describe interesting applications of CBMC.
Error explanation and localization
-
Mutation-Based Lifted Repair of Software Product Lines
CBMC is used in a lifted repair algorithm for program families based on code mutations. -
CFAULTS: Model-Based Diagnosis for Fault Localization in C with Multiple Test
Cases
CBMC is used to create Max-SAT formulas for fault 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
-
Formal Verification of Conventionally Qualified Safety Critical
Systems
The paper describes the application of CBMC to a library of function blocks for the TPLC32, which have previously been SG-D25 qualified. -
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 analyzels
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
-
An Extensive Investigation of Condition Reachability using CBMC: Study on Negative Results
CBMC is used to study how often structural test coverage metrics are impossible to satisfy on a large set of general-purpose C programs. - 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
- mlkem-native
CBMC is used to prove absence of various classes of undefined behaviour, including out of bounds memory accesses and integer overflows. -
Verifying Memory Confidentiality and Integrity of Intel TDX Trusted Execution
Environments
CBMC is used to prove memory confidentiality and integrity of an Intel TDX implementation. -
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.