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
相关论文
共 12 条
[1]  
[Anonymous], Rust Language
[2]  
Barrett C., 2016, The Satisfiability Modulo Theories Library (SMT-LIB)
[3]  
Bjorner N., 2012, P SMT IJCAR, P3
[4]   Horn Clause Solvers for Program Verification [J].
Bjorner, Nikolaj ;
Gurfinkel, Arie ;
McMillan, Ken ;
Rybalchenko, Andrey .
FIELDS OF LOGIC AND COMPUTATION II: ESSAYS DEDICATED TO YURI GUREVICH ON THE OCCASION OF HIS 75TH BIRTHDAY, 2015, 9300 :24-51
[5]   ICE-Based Refinement Type Discovery for Higher-Order Functional Programs [J].
Champion, Adrien ;
Chiba, Tomoya ;
Kobayashi, Naoki ;
Sato, Ryosuke .
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2018, PT I, 2018, 10805 :365-384
[6]   Z3: An efficient SMT solver [J].
de Moura, Leonardo ;
Bjorner, Nikolaj .
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 2008, 4963 :337-340
[7]   Learning Invariants using Decision Trees and Implication Counterexamples [J].
Garg, Pranav ;
Neider, Daniel ;
Madhusudan, P. ;
Roth, Dan .
ACM SIGPLAN NOTICES, 2016, 51 (01) :499-512
[8]  
Garg P, 2014, LECT NOTES COMPUT SC, V8559, P69, DOI 10.1007/978-3-319-08867-9_5
[9]  
Hoder Krystof, 2012, Theory and Applications of Satisability Testing-SAT 2012, P157, DOI [10.1007/978-3-642-31612-813, DOI 10.1007/978-3-642-31612-813]
[10]  
Hojjat Hossein, 2012, FM 2012: Formal Methods. Proceedings of the 18th International Symposium, P247, DOI 10.1007/978-3-642-32759-9_21