Harrsh: A Tool for Unied Reasoning about Symbolic-Heap Separation Logic

14 pages•Published: November 18, 2018

Jens Katelaan, Christoph Matheja, Thomas Noll and Florian Zuleger

Abstract

In this tool paper we present Harrsh – a tool for unified reasoning about symbolic-heap separation logic. Harrsh supports the analysis of robustness properties of the symbolic heap fragment of separation logic with user-defined inductive predicates. Robustness properties, such as satisfiability, reachability, and acyclicity, are important for a wide range of reasoning tasks in automated program analysis and verification based on separation logic. Harrsh makes use of heap automata, which offer a generic approach to reasoning about robustness properties. We report on experimental results for several robustness properties taken from the literature and compare against satisfiability checkers participating in a recent competition. We conclude that a generic approach to checking robustness is feasible and promising for the extension to further properties of interest.

In: Gilles Barthe, Konstantin Korovin, Stephan Schulz, Martin Suda, Geoff Sutcliffe and Margus Veanes (editors). LPAR-22 Workshop and Short Paper Proceedings, vol 9, pages 23-36.

Links:	https://easychair.org/publications/paper/6vZt
	https://doi.org/10.29007/qwd8

BibTeX entry

@inproceedings{LPAR-IWIL2018:Harrsh_Tool_Unied_Reasoning,
  author    = {Jens Katelaan and Christoph Matheja and Thomas Noll and Florian Zuleger},
  title     = {Harrsh: A Tool for Unied Reasoning about Symbolic-Heap Separation Logic},
  booktitle = {LPAR-22 Workshop and Short Paper Proceedings},
  editor    = {Gilles Barthe and Konstantin Korovin and Stephan Schulz and Martin Suda and Geoff Sutcliffe and Margus Veanes},
  series    = {Kalpa Publications in Computing},
  volume    = {9},
  publisher = {EasyChair},
  bibsource = {EasyChair, https://easychair.org},
  issn      = {2515-1762},
  url       = {/publications/paper/6vZt},
  doi       = {10.29007/qwd8},
  pages     = {23-36},
  year      = {2018}}

Download PDF Open PDF in browser