HoIce: An ICE-Based Non-linear Horn Clause Solver

被引：22

作者：

Champion, Adrien ^{[1
]}

Kobayashi, Naoki ^{[1
]}

Sato, Ryosuke ^{[2
]}

机构：

[1] Univ Tokyo, Tokyo, Japan

[2] Kyushu Univ, Fukuoka, Japan

来源：

PROGRAMMING LANGUAGES AND SYSTEMS, APLAS 2018 | 2018年 / 11275卷

关键词：

D O I：

10.1007/978-3-030-02768-1_8

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

The ICE framework is a machine-learning-based technique originally introduced for inductive invariant inference over transition systems, and building on the supervised learning paradigm. Recently, we adapted the approach to non-linear Horn clause solving in the context of higher-order program verification. We showed that we could solve more of our benchmarks (extracted from higher-order program verification problems) than other state-of-the-art Horn clause solvers. This paper discusses some of the many improvements we recently implemented in HoIce, our implementation of this generalized ICE framework.

引用

页码：146 / 156

页数：11