The Horn-ICE verification toolkit is a fully automated program verifier built on top of Microsoft Boogie. Horn-ICE combines deductive verification techniques with inductive machine learning technology to infer contracts and invariants in a fully automated manner. The toolkit features various specialized learning algorithms, including the classical Houdini algorithm, Sorcar, and novel algorithms for learning decision trees. The source code is available on GitHub.
Try it out yourself or have a look at our examples:
This website is an early version. Please contact us for comments or report issues to GitHub.