Contents Menu Expand Light mode Dark mode Auto light/dark, in light mode Auto light/dark, in dark mode Skip to content
CppVerify
Light Logo Dark Logo
CppVerify

Book

  • The CppVerify Book
    • Part I — Foundations
      • Chapter 1 — Correctness and trust
      • Chapter 2 — The limits of testing
      • Chapter 3 — Logic and specifications
      • Chapter 4 — Hoare logic
      • Chapter 5 — Invariants and loops
      • Chapter 6 — Ghost reasoning and lemmas
      • Chapter 7 — Memory, aliasing, and frame conditions
      • Chapter 8 — SMT solvers and automation
    • Part II — CppVerify
      • Chapter 9 — Why CppVerify on Clang
      • Chapter 10 — Getting started
      • Chapter 11 — Your first verified function
      • Chapter 12 — Loops in practice
      • Chapter 13 — Spec and proof functions
      • Chapter 14 — Pointers, frames, and modifies
      • Chapter 15 — Toolchain and flags
      • Chapter 16 — When verification fails
      • Chapter 17 — Backends, modular calls, and debugging
      • Chapter 18 — Undefined behavior
      • Chapter 19 — Dynamic storage and lifetime

Reference

  • Language reference
    • Contract syntax
    • Contract expressions
    • Functions and loops
    • Ghost, spec, and proofs
    • Structs and type invariants
    • Pointers
    • Dynamic storage
    • Integers
    • Commands and flags
    • Current limitations and C++ readiness
  • C++ API reference

Case studies

  • Case studies
    • LLVM ULEB128
    • UTF-8 validation
    • Binary search
Back to top
View this page
Edit this page

Case studies¶

Measured verification artifacts built from real systems algorithms.

  • LLVM ULEB128
  • UTF-8 validation
  • Binary search
Next
LLVM ULEB128
Previous
C++ API reference
Copyright © 2026, CppVerify contributors
Made with Sphinx and @pradyunsg's Furo