Inferring simple solutions to recursion-free horn clauses via sampling

Hiroshi Unno, Tachio Terauchi

研究成果: Conference contribution

4 被引用数 (Scopus)

抄録

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.

本文言語English
ホスト出版物のタイトル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
編集者Cesare Tinelli, Christel Baier
出版社Springer Verlag
ページ149-163
ページ数15
ISBN(電子版)9783662466803
DOI
出版ステータスPublished - 2015
外部発表はい
イベント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
継続期間: 2015 4 112015 4 18

出版物シリーズ

名前Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
9035
ISSN(印刷版)0302-9743
ISSN(電子版)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
国/地域United Kingdom
CityLondon
Period15/4/1115/4/18

ASJC Scopus subject areas

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

フィンガープリント

「Inferring simple solutions to recursion-free horn clauses via sampling」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル