GRASShopper: Complete heap verification with mixed specifications

Ruzica Piskac, Thomas Wies, Damien Zufferey

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

Abstract

We present GRASShopper, a tool for compositional verification of heap-manipulating programs against user-provided specifications. What makes our tool unique is its decidable specification language, which supports mixing of assertions expressed in separation logic and first-order logic. The user of the tool can thus take advantage of the succinctness of separation logic specifications and the discipline of local reasoning. Yet, at the same time, she can revert to classical logic in the cases where decidable separation logic fragments are less suited, such as reasoning about constraints on data and heap structures with complex sharing. We achieve this combination of specification languages through a translation to programs whose specifications are expressed in a decidable fragment of first-order logic called GRASS. This logic is well-suited for automation using satisfiability modulo theory solvers. Unlike other tools that provide similar features, our decidability guarantees enable GRASShopper to produce detailed counterexamples for incorrect or underspecified programs.We have found this feature to be invaluable when debugging specifications. We present the underlying philosophy of the tool, describe the major technical challenges, and discuss implementation details. We conclude with an evaluation that considers challenging benchmarks such as sorting algorithms and a union/find data structure.

Original languageEnglish (US)
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems - 20th Int. Conf., TACAS 2014, Held as Part of the European Joint Conf. on Theory and Practice of Software, ETAPS 2014, Proc.
PublisherSpringer Verlag
Pages124-139
Number of pages16
ISBN (Print)9783642548611
DOIs
StatePublished - 2014
Event20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2014 - Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014 - v, France
Duration: Apr 5 2014Apr 13 2014

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8413 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2014 - Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014
CountryFrance
Cityv
Period4/5/144/13/14

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'GRASShopper: Complete heap verification with mixed specifications'. Together they form a unique fingerprint.

  • Cite this

    Piskac, R., Wies, T., & Zufferey, D. (2014). GRASShopper: Complete heap verification with mixed specifications. In Tools and Algorithms for the Construction and Analysis of Systems - 20th Int. Conf., TACAS 2014, Held as Part of the European Joint Conf. on Theory and Practice of Software, ETAPS 2014, Proc. (pp. 124-139). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8413 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-642-54862-8_9