Inferring simple solutions to recursion-free horn clauses via sampling

Hiroshi Unno, Tachio Terauchi

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

4 Citations (Scopus)

Abstract

Recursion-free Horn-clause constraints have received much recent attention in the verification community. It extends Craig interpolation, and is proposed as a unifying formalism for expressing abstraction refinement. In abstraction refinement, it is often desirable to infer “simple” refinements, and researchers have studied techniques for inferring simple Craig interpolants. Drawing on the line of work, this paper presents a technique for inferring simple solutions to recursion-free Hornclause constraints. Our contribution is a constraint solving algorithm that lazily samples fragments of the given constraints whose solution spaces are used to form a simple solution for the whole. We have implemented a prototype of the constraint solving algorithm in a verification tool, and have confirmed that it is able to infer simple solutions that aid the verification process.

Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings
PublisherSpringer Verlag
Pages149-163
Number of pages15
Volume9035
ISBN (Electronic)9783662466803
DOIs
Publication statusPublished - 2015
Externally publishedYes
Event21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015 - London, United Kingdom
Duration: 2015 Apr 112015 Apr 18

Publication series

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

Other

Other21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015
CountryUnited Kingdom
CityLondon
Period15/4/1115/4/18

Fingerprint

Horn clause
Recursion
Sampling
Constraint Solving
Refinement
Interpolation
Interpolants
Fragment
Interpolate
Prototype
Line

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Unno, H., & Terauchi, T. (2015). Inferring simple solutions to recursion-free horn clauses via sampling. In Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings (Vol. 9035, pp. 149-163). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9035). Springer Verlag. https://doi.org/10.1007/978-3-662-46681-0_10

Inferring simple solutions to recursion-free horn clauses via sampling. / Unno, Hiroshi; Terauchi, Tachio.

Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings. Vol. 9035 Springer Verlag, 2015. p. 149-163 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9035).

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

Unno, H & Terauchi, T 2015, Inferring simple solutions to recursion-free horn clauses via sampling. in Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings. vol. 9035, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9035, Springer Verlag, pp. 149-163, 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, United Kingdom, 15/4/11. https://doi.org/10.1007/978-3-662-46681-0_10
Unno H, Terauchi T. Inferring simple solutions to recursion-free horn clauses via sampling. In Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings. Vol. 9035. Springer Verlag. 2015. p. 149-163. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-662-46681-0_10
Unno, Hiroshi ; Terauchi, Tachio. / Inferring simple solutions to recursion-free horn clauses via sampling. Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings. Vol. 9035 Springer Verlag, 2015. pp. 149-163 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{9db6586e01aa45e194d2ea2881099099,
title = "Inferring simple solutions to recursion-free horn clauses via sampling",
abstract = "Recursion-free Horn-clause constraints have received much recent attention in the verification community. It extends Craig interpolation, and is proposed as a unifying formalism for expressing abstraction refinement. In abstraction refinement, it is often desirable to infer “simple” refinements, and researchers have studied techniques for inferring simple Craig interpolants. Drawing on the line of work, this paper presents a technique for inferring simple solutions to recursion-free Hornclause constraints. Our contribution is a constraint solving algorithm that lazily samples fragments of the given constraints whose solution spaces are used to form a simple solution for the whole. We have implemented a prototype of the constraint solving algorithm in a verification tool, and have confirmed that it is able to infer simple solutions that aid the verification process.",
author = "Hiroshi Unno and Tachio Terauchi",
year = "2015",
doi = "10.1007/978-3-662-46681-0_10",
language = "English",
volume = "9035",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "149--163",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings",
address = "Germany",

}

TY - GEN

T1 - Inferring simple solutions to recursion-free horn clauses via sampling

AU - Unno, Hiroshi

AU - Terauchi, Tachio

PY - 2015

Y1 - 2015

N2 - Recursion-free Horn-clause constraints have received much recent attention in the verification community. It extends Craig interpolation, and is proposed as a unifying formalism for expressing abstraction refinement. In abstraction refinement, it is often desirable to infer “simple” refinements, and researchers have studied techniques for inferring simple Craig interpolants. Drawing on the line of work, this paper presents a technique for inferring simple solutions to recursion-free Hornclause constraints. Our contribution is a constraint solving algorithm that lazily samples fragments of the given constraints whose solution spaces are used to form a simple solution for the whole. We have implemented a prototype of the constraint solving algorithm in a verification tool, and have confirmed that it is able to infer simple solutions that aid the verification process.

AB - Recursion-free Horn-clause constraints have received much recent attention in the verification community. It extends Craig interpolation, and is proposed as a unifying formalism for expressing abstraction refinement. In abstraction refinement, it is often desirable to infer “simple” refinements, and researchers have studied techniques for inferring simple Craig interpolants. Drawing on the line of work, this paper presents a technique for inferring simple solutions to recursion-free Hornclause constraints. Our contribution is a constraint solving algorithm that lazily samples fragments of the given constraints whose solution spaces are used to form a simple solution for the whole. We have implemented a prototype of the constraint solving algorithm in a verification tool, and have confirmed that it is able to infer simple solutions that aid the verification process.

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

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

U2 - 10.1007/978-3-662-46681-0_10

DO - 10.1007/978-3-662-46681-0_10

M3 - Conference contribution

AN - SCOPUS:84926629327

VL - 9035

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

SP - 149

EP - 163

BT - Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings

PB - Springer Verlag

ER -