Alloy Analyzer vs CBMC
Alloy Analyzer
alloytools.orgCBMC
diffblue.github.ioSide by side
| Figure | Alloy Analyzer | CBMC |
|---|---|---|
| Price from | Free | Free |
| Free plan | Yes | Yes |
| Free trial | — | — |
| Open source | — | — |
| Windows | Yes | Yes |
| macOS | Yes | Yes |
| Linux | Yes | Yes |
| API | Yes | — |
| Self-hosted | — | Yes |
| Plans published | 1 | 1 |
| Spec score · Formal Verification Tools | 8.1 (#6) | 8.1 (#8) |
| Platforms | The download page identifies Alloy 6.2.0 and says it includes a version for macOS High Sierra; it also describes running the JAR with Java. | The installation guide points to installation instructions for macOS, Ubuntu, Windows, and Docker. |
| Purpose | Alloy is a language for describing evolving structures, and the Alloy Analyzer explores models by finding structures that satisfy constraints or counterexamples to properties. | CBMC is a bounded model checker for C and C++ programs that explores possible execution paths and checks assertions. |
Plans
In their own words
Alloy Analyzer
Alloy Analyzer is a free model-checking tool for describing systems in the Alloy language and exploring the structures those descriptions permit. It searches for structures that satisfy constraints and for counterexamples to properties. Models can represent collections of structures that change over time, including security configurations and switching network topologies. The Analyzer presents results graphically, with appearance options that can be tailored to a domain. Alloy 6 adds mutable state, temporal logic, and temporal model checking; that checking requires NuSMV or nuXmv to be installed and available in PATH. The self-contained executable includes the Pardinus/Kodkod model finder, SAT solvers, the standard Alloy library, tutorial examples, and source code. The same JAR can be used as an API in other applications. Sterling adds a web-based visualizer with graph and table views, customizable and extendable with JavaScript. Alloy is self-hosted, supports Linux, macOS, Windows, and API use, and is maintained by volunteers.
CBMC
CBMC is a bounded model checker for C and C++ programs. It explores execution paths to check assertions, including array bounds, pointer safety, exceptions, and some undefined behavior such as signed integer overflow. Its analysis unwinds loops before sending the resulting equation to a decision procedure, and inputs may need a bounded size. The repository lists C89, C99, most of C11, C17, C23, GCC and Visual Studio extensions, and SystemC through Scoot; the listed input languages also include Java bytecode. CBMC supports contracts and can produce counterexamples. Its incremental SMT2 backend works with SMT-LIB 2.6-compliant solvers, with Z3 and CVC5 as examples. Distribution options include Homebrew instructions for macOS, Ubuntu DEB packages, Windows MSI installers, and Docker images. goto-cc can replace gcc or cl.exe in Makefiles to collect project models. The guide discusses routine development and continuous integration use. CBMC is free under the 4-clause BSD license.