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.
aware debugging for mobile applications
CBMC is used to debug mobile applications.
- Error Explanation with
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.
- 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.
Partial Translation Verification for Untrusted
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.
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
CBMC is used on various arithmetic circuit models.
Equivalence Checking between Function Block
Diagrams and C Programs Using
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
- CBMC is used to verify a MISRA-C implementation of an adaptive exterior light system (ELS) and a speed control system (SCS).
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
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
- 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
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
lsin busybox, with a comparison with concolic testing
Crowdsourcing Program Preconditions via a Classification
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.
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
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.
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
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
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.
- 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.
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.
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.
- Proving JDK's Dual Pivot Quicksort Correct CBMC is used to discharge hard VCCs in a proof of JDK's sorting.
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.