Пакет cbmc: Информация

CBMC is a Bounded Model Checker for C and C++ programs. It supports C89,
C99, most of C11 and most compiler extensions provided by gcc and Visual
Studio. It also supports SystemC using Scoot. It allows verifying array
bounds (buffer overflows), pointer safety, exceptions and user-specified
assertions. Furthermore, it can check C and C++ for consistency with
other languages, such as Verilog. The verification is performed by
unwinding the loops in the program and passing the resulting equation
to a decision procedure.

         OOOOOOOOO
      OOO  .   .  OOO
     OO     \ /  OOOOO
    OO    `/ ! OOO   OO
    OO    | :OOO|    OO
    OO   ~|OOO: |~   OO
     OO  OOO_:_/ \  OO
      OOOO        OOO
        OOOOOOOOOOO