Boogie is a modeling language, intended as a layer on which to build program verifiers for other languages.
