Higher-order Program Verification as Satisfiability Modulo Theories with Algebraic Data-types

Nikolaj Bjorner, Ken McMillan, Andrey Rybalchenko

We report on work in progress on automatic procedures for proving properties of programs written in higher-order functional languages. Our approach encodes higher-order programs di…