Steering interpolants generation with efficient interpolation abstraction exploration

Xiaozhen Zhang, Weiqiang Kong, Jianguo Jiang, Gang Hou, Akira Fukuda

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

抜粋

Craig interpolation has emerged as an effective approximation method and can be widely applied in hardware and software model checking. Since the quality of interpolants can critically affect the success and failure, or convergence and divergence of model checking, researchers have put forward a novel and flexible interpolation abstraction-based technique to guide the computation of promising interpolants. In this technique, abstraction lattice is constructed to arrange families of interpolation abstraction for improving the quality of resulting interpolants. However, the original search strategy to explore an abstraction lattice is not efficient when abstraction lattice enlarges and the elapsed time to perform multiple search on the same abstraction lattice is obviously distinct for many problems. In this paper, in order to alleviate these problems, we propose a top-down search space pruning-based algorithm to search the abstraction lattice and implement this algorithm in the well-known model checker Eldarica. We conduct experiments on 179 benchmarks to compare our algorithm respectively against the original search algorithm in Eldarica and the state-of-the-art SMT solver Z3. The experimental results show that our algorithm performs much better in the sense that it is more efficient than Eldarica for most of the benchmarks and it can solve much more benchmarks than Z3.

元の言語英語
ホスト出版物のタイトルProceedings - 2019 13th International Symposium on Theoretical Aspects of Software Engineering, TASE 2019
出版者Institute of Electrical and Electronics Engineers Inc.
ページ113-120
ページ数8
ISBN(電子版)9781728133423
DOI
出版物ステータス出版済み - 7 2019
イベント13th International Symposium on Theoretical Aspects of Software Engineering, TASE 2019 - Guilin, 中国
継続期間: 7 29 20197 31 2019

出版物シリーズ

名前Proceedings - 2019 13th International Symposium on Theoretical Aspects of Software Engineering, TASE 2019

会議

会議13th International Symposium on Theoretical Aspects of Software Engineering, TASE 2019
中国
Guilin
期間7/29/197/31/19

All Science Journal Classification (ASJC) codes

  • Safety, Risk, Reliability and Quality
  • Computational Theory and Mathematics
  • Software
  • Information Systems and Management

フィンガープリント Steering interpolants generation with efficient interpolation abstraction exploration' の研究トピックを掘り下げます。これらはともに一意のフィンガープリントを構成します。

  • これを引用

    Zhang, X., Kong, W., Jiang, J., Hou, G., & Fukuda, A. (2019). Steering interpolants generation with efficient interpolation abstraction exploration. : Proceedings - 2019 13th International Symposium on Theoretical Aspects of Software Engineering, TASE 2019 (pp. 113-120). [8913993] (Proceedings - 2019 13th International Symposium on Theoretical Aspects of Software Engineering, TASE 2019). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/TASE.2019.00-11