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 7 articles )
Showing results 1 to 7 of 7.
- Champion, Adrien; Chiba, Tomoya; Kobayashi, Naoki; Sato, Ryosuke: ICE-based refinement type discovery for higher-order functional programs (2020)
- Milicevic, Aleksandar; Near, Joseph P.; Kang, Eunsuk; Jackson, Daniel: Alloy*: a general-purpose higher-order relational constraint solver (2019)
- 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