Lattice-Based Refinement in Bounded Model Checking

Karine Even-Mendoza, Sepideh Asadi, Antti Hyyvarinen, Hana Chockler, Natasha Sharygina

Research output: Chapter in Book/Report/Conference proceedingConference paperpeer-review

1 Citation (Scopus)
56 Downloads (Pure)

Abstract

In this paper we present an algorithm for bounded model checking with SMT solvers of programs with library functions—either standard or user-defined. Typically, if the program correctness depends on the output of a library function, the model-checking process either treats this function as an uninterpreted function, or is required to use a theory under which the function in question is fully defined. The former approach leads to numerous spurious counter-examples, whereas the later faces the danger of the state-explosion problem, where the resulting formula is too large to be solved by means of modern SMT solvers.
We extend the approach of user-defined summaries and propose to represent the set of existing summaries for a given library function as a lattice of subsets of summaries, with the meet and join operations defined as intersection and union, respectively. The refinement process is then triggered by the lattice traversal, where in each node the SMT solver uses the subset of SMT summaries stored in this node to search for a satisfying assignment. The direction of the traversal is determined by the results of the concretisation of an abstract counterexample obtained at the current node. Our experimental results demonstrate that this approach allows to solve a number of instances that were previously unsolvable by the existing bounded model-checkers.
Original languageEnglish
Title of host publicationVerified Software. Theories, Tools, and Experiments (VSTTE) 2018
Place of PublicationSwitzerland
PublisherSpringer
Pages50-68
Number of pages19
ISBN (Electronic)978-3-030-03592-1
ISBN (Print)978-3-030-03591-4
DOIs
Publication statusPublished - 18 Jul 2018

Fingerprint

Dive into the research topics of 'Lattice-Based Refinement in Bounded Model Checking'. Together they form a unique fingerprint.

Cite this