Steering interpolants generation with efficient interpolation abstraction exploration

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

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

Abstract

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.

Original languageEnglish
Title of host publicationProceedings - 2019 13th International Symposium on Theoretical Aspects of Software Engineering, TASE 2019
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages113-120
Number of pages8
ISBN (Electronic)9781728133423
DOIs
Publication statusPublished - Jul 2019
Event13th International Symposium on Theoretical Aspects of Software Engineering, TASE 2019 - Guilin, China
Duration: Jul 29 2019Jul 31 2019

Publication series

NameProceedings - 2019 13th International Symposium on Theoretical Aspects of Software Engineering, TASE 2019

Conference

Conference13th International Symposium on Theoretical Aspects of Software Engineering, TASE 2019
CountryChina
CityGuilin
Period7/29/197/31/19

All Science Journal Classification (ASJC) codes

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

Fingerprint Dive into the research topics of 'Steering interpolants generation with efficient interpolation abstraction exploration'. Together they form a unique fingerprint.

Cite this