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

Adrien Champion, Naoki Kobayashi, Ryosuke Sato

研究成果: Chapter in Book/Report/Conference proceedingConference contribution

7 被引用数 (Scopus)

抄録

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.

本文言語英語
ホスト出版物のタイトルProgramming Languages and Systems - 16th Asian Symposium, APLAS 2018, Proceedings
編集者Sukyoung Ryu
出版社Springer Verlag
ページ146-156
ページ数11
ISBN(印刷版)9783030027674
DOI
出版ステータス出版済み - 2018
イベント16th Asian Symposium on Programming Languages and Systems, APLAS 2018 - Wellington, ニュージ―ランド
継続期間: 12 2 201812 6 2018

出版物シリーズ

名前Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
11275 LNCS
ISSN(印刷版)0302-9743
ISSN(電子版)1611-3349

その他

その他16th Asian Symposium on Programming Languages and Systems, APLAS 2018
国/地域ニュージ―ランド
CityWellington
Period12/2/1812/6/18

All Science Journal Classification (ASJC) codes

  • 理論的コンピュータサイエンス
  • コンピュータ サイエンス(全般)

フィンガープリント

「HoIce: An ICE-Based Non-linear Horn Clause Solver」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル