Boogie vs UPPAAL

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.

UPPAAL is an integrated environment for modeling, simulating, and verifying real-time systems as networks of timed automata. Its language supports clock and data variables, including bounded integers and arrays. The model checker uses symbolic state-space exploration for invariant and reachability properties and can produce diagnostic traces. Statistical Model Checking estimates probabilities, compares a probability with a value, or compares two probabilities. UPPAAL Stratego supports generating, optimizing, comparing, and exploring strategies for stochastic priced timed games. Related tools include CORA, TRON, TIGA, ECDAR, and COSHY for cost-optimal analysis, testing, timed games, refinement, and hybrid-system control. Typical applications include real-time controllers and timing-critical communication protocols. Desktop packages support Windows, macOS, and Linux, including macOS x86_64 and Aarch64. The graphical interface needs Java 17 or later; verifyta runs without Java. Academic users register for a free license key, retrieved over the internet. Commercial and other non-academic use requires a separate license.