The C Bounded Model Checker: Criminally Underused

This page summarizes the projects mentioned and recommended in the original post on news.ycombinator.com

InfluxDB - Power Real-Time Data Analytics at Scale
Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
www.influxdata.com
featured
SaaSHub - Software Alternatives and Reviews
SaaSHub helps you find the best software and product alternatives
www.saashub.com
featured
  • dmd

    dmd D Programming Language compiler

  • Thank you for the explanation.

    I agree that if one isn't going to enhance C, one is going to have to resort to these tools.

    C gets new features now and then. Why not add something incredibly useful, like the slice proposal? Instead, C23 got enhanced with the crazy Unicode identifiers. Richard Cattermole has been adding them to D's C support, requiring 6000 lines of code!!

    https://github.com/dlang/dmd/pull/15307

    The entire C parser is 6000 lines of code:

    https://github.com/dlang/dmd/blob/master/compiler/src/dmd/cp...

  • coreHTTP

    Client implementation of a subset of HTTP 1.1 protocol designed for embedded devices.

  • One of the examples they gave was an HTTP client, which would be a surprisingly non-toy example, so I looked at what they actually did in the code (https://github.com/FreeRTOS/coreHTTP/tree/main/test/cbmc).

    Not that I'm an expert in processing what exactly is being tested, but it basically looks only able to prove that an individual function doesn't overrun buffers. If you tell it to assume that overflows can't happen (!). So I'm not impressed.

  • InfluxDB

    Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.

    InfluxDB logo
  • c-semantics

    Semantics of C in K

  • tis-interpreter

    An interpreter for finding subtle bugs in programs written in standard C

  • kani

    Kani Rust Verifier

  • This is also the backend for Kani - Amazon's formal verification tool for Rust.

    https://github.com/model-checking/kani

  • cbmc

    C Bounded Model Checker

  • https://github.com/diffblue/cbmc/issues/7732 I'll note that some form of undefined behavior checking / documentation is on the roadmap for the next major version

NOTE: The number of mentions on this list indicates mentions on common posts plus user suggested alternatives. Hence, a higher number means a more popular project.

Suggest a related project

Related posts

  • Results of the Grand C++ Error Explosion Competition

    1 project | news.ycombinator.com | 6 May 2024
  • A History of C Compilers – Part 1: Performance, Portability and Freedom

    1 project | news.ycombinator.com | 5 May 2024
  • 7 Programming Languages Every Cloud Engineer Should Know in 2024!

    4 projects | dev.to | 5 Mar 2024
  • DMD Compiler as a Library: A Call to Arms

    3 projects | news.ycombinator.com | 22 Feb 2024
  • The OpenD Programming Language (fork of D)

    2 projects | news.ycombinator.com | 5 Jan 2024