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: