HMC: Verifying functional programs using abstract interpreters. 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.
Keywords for this software
References in zbMATH (referenced in 5 articles )
Showing results 1 to 5 of 5.
- Watanabe, Keiichi; Sato, Ryosuke; Tsukada, Takeshi; Kobayashi, Naoki: Automatically disproving fair termination of higher-order functional programs (2016)
- Bjørner, Nikolaj; Gurfinkel, Arie; McMillan, Ken; Rybalchenko, Andrey: Horn clause solvers for program verification (2015)
- Rümmer, Philipp; Hojjat, Hossein; Kuncak, Viktor: On recursion-free Horn clauses and Craig interpolation (2015)
- Kuwahara, Takuya; Terauchi, Tachio; Unno, Hiroshi; Kobayashi, Naoki: Automatic termination verification for higher-order functional programs (2014)
- Jhala, Ranjit; Majumdar, Rupak; Rybalchenko, Andrey: HMC: Verifying functional programs using abstract interpreters (2011) ioport