Abstract
We present Dsolve, a verification tool for OCaml. Dsolve automates verification by inferring “Liquid” refinement types that are expressive enough to verify a variety of complex safety properties.
This work was supported by NSF grants CCF-0644361, CNS-0720802, CCF-0702603, and a gift from Microsoft Research.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
**, H., Pfenning, F.: Eliminating array bound checking through dependent types. In: PLDI (1998)
Cui, S., Donnelly, K., **, H.: ATS: A language that combines programming with theorem proving. In: Gramlich, B. (ed.) FroCos 2005. LNCS (LNAI), vol. 3717, pp. 310–320. Springer, Heidelberg (2005)
Bengtson, J., Bhargavan, K., Fournet, C., Gordon, A.D., Maffeis, S.: Refinement types for secure implementations. In: CSF (2008)
Dunfield, J.: A Unified System of Type Refinements. PhD thesis, Carnegie Mellon University, Pittsburgh, PA, USA (2007)
Rondon, P., Kawaguchi, M., Jhala, R.: Liquid types. In: PLDI (2008)
Kawaguchi, M., Rondon, P., Jhala, R.: Type-based data structure verification. In: PLDI, pp. 304–315 (2009)
de Moura, L., Bjørner, N.: Z3: An efficient smt solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
**, H.: DML code examples, http://www.cs.bu.edu/fac/hwxi/DML/
Filliátre, J.C.: Bitv, http://www.lri.fr/~filliatr/software.en.html
de Alfaro, L.: Vec, http://www.dealfaro.com/~luca/vec.html
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kawaguchi, M., Rondon, P.M., Jhala, R. (2010). Dsolve: Safety Verification via Liquid Types. In: Touili, T., Cook, B., Jackson, P. (eds) Computer Aided Verification. CAV 2010. Lecture Notes in Computer Science, vol 6174. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14295-6_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-14295-6_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14294-9
Online ISBN: 978-3-642-14295-6
eBook Packages: Computer ScienceComputer Science (R0)