FreeBoogie is a Java clone of the World's Best Program Verifier. It checks the correctness of Boogie programs. There are a few frontends for static analysis/verification that target the Boogie language: Spec#, VCC, B2BPL. If you consider implementing a static analysis, then take a look at Boogie.
Copyright © 2013 Black Duck Software, Inc. and its contributors, Some Rights Reserved. Unless otherwise marked, this work is licensed under a Creative Commons Attribution 3.0 Unported License . Ohloh ® and the Ohloh logo are trademarks of Black Duck Software, Inc. in the United States and/or other jurisdictions. All other trademarks are the property of their respective holders.