We present Dsolve, a verification tool for Ocaml, that automates verification by inferring ``Liquid" refinement types that are expressive enough to verify a variety of complex safety properties.
Proceedings of the 22nd Intl. Conference on Computer-Aided Verification (CAV), 2010.