activity
20102016
most citedHigher-order Program Verification as Satisfiability Modulo Theories with Algebraic Data-types

16 citations · 42 across the 9 of their papers we have counts for

collaborators
Showing cs.PLShow all

1 paper · 1 filter

cs.PL2010

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…