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
Volume8413 LNCS
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)03029743
ISSN (Electronic)16113349

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

Fingerprint

Heap
Separation Logic
Specification
Specifications
Specification languages
Specification Languages
First-order Logic
Fragment
Reasoning
Compositional Verification
Computability and decidability
Sorting algorithm
Classical Logic
Debugging
Decidability
Assertion
Sorting
Automation
Data structures
Counterexample

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

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. (Vol. 8413 LNCS, 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

GRASShopper : Complete heap verification with mixed specifications. / Piskac, Ruzica; Wies, Thomas; Zufferey, Damien.

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.. Vol. 8413 LNCS Springer Verlag, 2014. p. 124-139 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8413 LNCS).

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

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.. vol. 8413 LNCS, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8413 LNCS, Springer Verlag, pp. 124-139, 20th 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, 4/5/14. https://doi.org/10.1007/978-3-642-54862-8_9
Piskac R, Wies T, Zufferey D. 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.. Vol. 8413 LNCS. Springer Verlag. 2014. p. 124-139. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-54862-8_9
Piskac, Ruzica ; Wies, Thomas ; Zufferey, Damien. / GRASShopper : Complete heap verification with mixed specifications. 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.. Vol. 8413 LNCS Springer Verlag, 2014. pp. 124-139 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{f5189f188d994169a1b99f0acf779c66,
title = "GRASShopper: Complete heap verification with mixed specifications",
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.",
author = "Ruzica Piskac and Thomas Wies and Damien Zufferey",
year = "2014",
doi = "10.1007/978-3-642-54862-8_9",
language = "English (US)",
isbn = "9783642548611",
volume = "8413 LNCS",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "124--139",
booktitle = "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.",

}

TY - GEN

T1 - GRASShopper

T2 - Complete heap verification with mixed specifications

AU - Piskac, Ruzica

AU - Wies, Thomas

AU - Zufferey, Damien

PY - 2014

Y1 - 2014

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84900565643&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84900565643&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-54862-8_9

DO - 10.1007/978-3-642-54862-8_9

M3 - Conference contribution

SN - 9783642548611

VL - 8413 LNCS

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 124

EP - 139

BT - 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.

PB - Springer Verlag

ER -