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

Adrien Champion, Naoki Kobayashi, Ryosuke Sato

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

1 Citation (Scopus)

Abstract

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
Pages146-156
Number of pages11
ISBN (Print)9783030027674
DOIs
Publication statusPublished - Jan 1 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

Other

Other16th Asian Symposium on Programming Languages and Systems, APLAS 2018
CountryNew Zealand
CityWellington
Period12/2/1812/6/18

Fingerprint

Horn clause
Program Verification
Higher Order
Transition Systems
Supervised learning
Supervised Learning
Learning systems
Machine Learning
Paradigm
Benchmark
Invariant
Framework
Context

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Champion, A., Kobayashi, N., & Sato, R. (2018). HoIce: An ICE-Based Non-linear Horn Clause Solver. In S. Ryu (Ed.), Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Proceedings (pp. 146-156). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11275 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-030-02768-1_8

HoIce : An ICE-Based Non-linear Horn Clause Solver. / Champion, Adrien; Kobayashi, Naoki; Sato, Ryosuke.

Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Proceedings. ed. / Sukyoung Ryu. Springer Verlag, 2018. p. 146-156 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11275 LNCS).

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

Champion, A, Kobayashi, N & Sato, R 2018, HoIce: An ICE-Based Non-linear Horn Clause Solver. in S Ryu (ed.), Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11275 LNCS, Springer Verlag, pp. 146-156, 16th Asian Symposium on Programming Languages and Systems, APLAS 2018, Wellington, New Zealand, 12/2/18. https://doi.org/10.1007/978-3-030-02768-1_8
Champion A, Kobayashi N, Sato R. HoIce: An ICE-Based Non-linear Horn Clause Solver. In Ryu S, editor, Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Proceedings. Springer Verlag. 2018. p. 146-156. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-030-02768-1_8
Champion, Adrien ; Kobayashi, Naoki ; Sato, Ryosuke. / HoIce : An ICE-Based Non-linear Horn Clause Solver. Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Proceedings. editor / Sukyoung Ryu. Springer Verlag, 2018. pp. 146-156 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{02100464c0934af7a5cd30d662fc9a4d,
title = "HoIce: An ICE-Based Non-linear Horn Clause Solver",
abstract = "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.",
author = "Adrien Champion and Naoki Kobayashi and Ryosuke Sato",
year = "2018",
month = "1",
day = "1",
doi = "10.1007/978-3-030-02768-1_8",
language = "English",
isbn = "9783030027674",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "146--156",
editor = "Sukyoung Ryu",
booktitle = "Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Proceedings",
address = "Germany",

}

TY - GEN

T1 - HoIce

T2 - An ICE-Based Non-linear Horn Clause Solver

AU - Champion, Adrien

AU - Kobayashi, Naoki

AU - Sato, Ryosuke

PY - 2018/1/1

Y1 - 2018/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85057896051&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85057896051&partnerID=8YFLogxK

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

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

M3 - Conference contribution

AN - SCOPUS:85057896051

SN - 9783030027674

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 146

EP - 156

BT - Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Proceedings

A2 - Ryu, Sukyoung

PB - Springer Verlag

ER -