Dsolve: Safety Verification with Liquid Types

Ming Kawaguchi, Patrick Rondon, and Ranjit Jhala.

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.


PDF © 2010.