Alloy Analyzer vs Boogie

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.

Boogie is a modeling language and tool for building program verifiers for other languages. It accepts Boogie language input, can optionally infer invariants, and generates verification conditions for an SMT solver. Z3 is the default solver; CVC5 and Yices2 support is experimental. The Civl extension lets users model concurrent and distributed systems. Boogie is self-hosted and distributed as a.NET global tool through NuGet. It requires.NET and a supported SMT solver, and the NuGet listing identifies version 3.5.7 as targeting.NET 8.0 or higher. The project uses the MIT License and is free at free. The repository names VCC and HAVOC for C, along with Dafny, Chalice, Spec#, and Move verifiers, as projects built on Boogie. Yices2 has a stated constraint: it works for unquantified fragments such as arrays, arithmetic, and bitvectors, but not for quantifiers, generalized arrays, or datatypes. Users can ask questions or report issues through the project issue tracker, and contributions are accepted through pull requests.