Bounded Model Checking Higher-Order Programs

Yu-Yang Lin

We present two bounded model checking techniques for higher-order programs. The first technique is based on defunctionalization and points-to analysis for verification of higher-order terms with free variables of ground type. The second technique is based on game semantics and symbolic execution for verification of open terms with free variables of arbitrary order. The vehicle of study is a lambda-calculus with higher-order (general) references. Both techniques are proven sound and correct.