论文标题
高阶MSL角约束
Higher-Order MSL Horn Constraints
论文作者
论文摘要
Monadic浅线性（MSL）类是一阶角子句的可决定的片段，在世纪之交左右发现并重新发现，并应用于静态分析和验证。我们提出了一类新的高阶喇叭约束，将MSL扩展到高阶逻辑并制定基于解决方案的决策程序。高阶MSL角约束可以自然地捕获高阶程序中可能的复杂呼叫和返回模式，这使它们非常适合高阶程序验证。实际上，我们表明高阶MSL满意度问题和HOSS模型检查问题是可互换的，因此可以将高阶MSL视为基于约束的高阶模型检查方法。最后，我们描述了我们的决策程序的实现及其在验证套接式编程中的应用。
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.
