King's College London

Research portal

Lattice-Based Refinement in Bounded Model Checking

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

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

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
Publication statusPublished - 18 Jul 2018

Documents

  • VSTTE_2018

    VSTTE_2018.pdf, 711 KB, application/pdf

    8/11/2018

    Accepted author manuscript

    Other

King's Authors

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.

Download statistics

No data available

View graph of relations

© 2018 King's College London | Strand | London WC2R 2LS | England | United Kingdom | Tel +44 (0)20 7836 5454