Paper Info
Title
HMC: verifying functional programs using abstract interpreters
Abstract
We present Hindley-Milner-Cousots (HMC), an algorithm that reduces verification of safety properties of typed higher-order functional programs to interprocedural analysis for first-order imperative programs. HMC works as follows. First, it uses the type structure of the functional program to generate a set of logical refinement constraints whose satisfaction implies the safety of the source program. Next, it transforms the logical refinement constraints into a simple first-order imperative program and an invariant that holds iff the constraints are satisfiable. Finally, it uses an invariant generator for first-order imperative programs to discharge the invariant. We have implemented HMC and describe preliminary experimental results using two imperative checkers - ARMC and INTERPROC - to verify OCAML programs. By composing type-based reasoning grounded in program syntax and state-based reasoning grounded in abstract interpretation, HMC enables the fully automatic verification of programs written in modern programming languages.
Year
DOI
Venue
2011
10.1007/978-3-642-22110-1_38
CAV
Keywords
Field
DocType
imperative checker,simple first-order imperative program,logical refinement constraint,source program,program syntax,functional program,first-order imperative program,ocaml program,abstract interpreter,invariant generator,higher-order functional program,higher order functions,first order,functional programming,programming language,satisfiability
Programming language,Computer science,Abstract interpretation,Algorithm,Theoretical computer science,Interpreter,Invariant (mathematics),Syntax
Conference
Citations 
PageRank 
References 
27
1.01
24
Authors
3
Name
Order
Citations
PageRank
Ranjit Jhala12183111.68
Rupak Majumdar23401220.08
Andrey Rybalchenko3143968.53