Boogie vs NuSMV

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.

NuSMV is a self-hosted software tool for formally verifying finite state systems. It checks systems against CTL specifications and supports LTL and PSL model checking. NuSMV 2 combines BDD-based model checking with SAT-based bounded model checking. Its SMV input language supports hierarchical descriptions, reusable components and finite data types, including booleans, scalars, bit vectors and fixed arrays. Other capabilities include an interactive text shell, invariant analysis and partitioning methods; the SAT component can connect to the Minisat solver. The project describes uses in industrial design verification, custom verification tools and research into formal verification techniques. NuSMV runs on Linux, macOS and Windows, and version 2 is open source under LGPL v2.1. The project directs general questions and bug reports to its users mailing list, with a separate list for announcements. Its FAQ says there is no current tutorial for developers extending the tool. It also warns that processes are deprecated because they can behave incorrectly with relational constructs such as TRANS, INIT or INVAR.