Boogie is also the name of a tool. The tool accepts the Boogie language as input, optionally infers some invariants in the given Boogie program, and then generates verification conditions that are passed to an SMT solver. The default SMT solver is Z3.
The Boogie research project is being developed primarily in the RiSE group at Microsoft Research in Redmond. However, people at several other institutions make the open-source Boogie tool what it is.
Last modified 28 April 2025