Higher-Order MSL Horn Constraints

TL;DR

This paper introduces higher-order MSL Horn constraints, extending the decidable MSL class to higher-order logic, enabling effective verification of complex higher-order program behaviors.

Contribution

It develops a resolution-based decision procedure for higher-order MSL Horn constraints and demonstrates their applicability to higher-order program verification.

Findings

Higher-order MSL satisfiability is interreducible with HORS model checking.

The decision procedure is implemented and applied to verified socket programming.

Higher-order MSL effectively captures complex call-return patterns in higher-order programs.

Abstract

The monadic shallow linear (MSL) class is a decidable fragment of first-order Horn clauses that was discovered and rediscovered around the turn of the century, with applications in static analysis and verification. We propose a new class of higher-order Horn constraints which extend MSL to higher-order logic and develop a resolution-based decision procedure. Higher-order MSL Horn constraints can quite naturally capture the complex patterns of call and return that are possible in higher-order programs, which make them well suited to higher-order program verification. In fact, we show that the higher-order MSL satisfiability problem and the HORS model checking problem are interreducible, so that higher-order MSL can be seen as a constraint-based approach to higher-order model checking. Finally, we describe an implementation of our decision procedure and its application to verified socket programming.