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

Adrien Champion, Naoki Kobayashi, Ryosuke Sato

Research output: Chapter in Book/Report/Conference proceedingConference contribution

20 Citations (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.

Original languageEnglish
Title of host publicationProgramming Languages and Systems - 16th Asian Symposium, APLAS 2018, Proceedings
EditorsSukyoung Ryu
PublisherSpringer Verlag
Number of pages11
ISBN (Print)9783030027674
Publication statusPublished - 2018
Event16th Asian Symposium on Programming Languages and Systems, APLAS 2018 - Wellington, New Zealand
Duration: Dec 2 2018Dec 6 2018

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11275 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other16th Asian Symposium on Programming Languages and Systems, APLAS 2018
Country/TerritoryNew Zealand

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'HoIce: An ICE-Based Non-linear Horn Clause Solver'. Together they form a unique fingerprint.

Cite this