Boogie is an intermediate verification language, intended as a layer on which to build program verifiers for other languages. Several program verifiers have been built in this way, including the VCC and HAVOC verifiers for C and the verifiers for Dafny, Chalice, and Spec#. A previous version of the language was called BoogiePL. The current language (version 2) is currently known as just Boogie, which is also the name of the verification tool that takes Boogie programs as input.
If you want to learn more about the Boogie language and tool, good places to start are the Boogie 2 language reference manual and the Boogie tool architectural overview.
In their geneses, Boogie and Spec# were developed hand in hand. For this reason, the name Boogie has been used to describe Spec#-related things. In particular, the Spec# static program verifier, which translates compiled Spec# programs (.NET bytecode) into Boogie, has been called Boogie, but the Spec# verifier is nowadays a separate tool (built on Boogie) called SscBoogie. Finally, Spec# uses an ownership-based discipline for handling object invariants. This discipline is known as the Boogie methodology, but it is tied only to Spec# and its bytecode translator, not to the Boogie verification language.
Boogie has proven to be a great platform on top of which to implement other verification systems. Here is a partial list of such projects. If you know of others that should appear here, please let us know!