HMC: Verifying Functional Programs Using Abstract Interpreters

Ranjit Jhala, Rupak Majumdar, Andrey Rybalchenko

We present Hindley-Milner-Cousots (HMC), an algorithm that allows any interprocedural analysis for first-order imperative programs to be used to verify safety properties of typed h…