| ||||
| ||||
![]() Title:Harrsh: A Tool for Unied Reasoning about Symbolic-Heap Separation Logic Conference:IWIL-2018 Tags:heap automata, inductive definitions, robustness properties, satisfiability and symbolic-heap separation logic 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 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. Harrsh: A Tool for Unied Reasoning about Symbolic-Heap Separation Logic ![]() Harrsh: A Tool for Unied Reasoning about Symbolic-Heap Separation Logic | ||||
Copyright © 2002 – 2025 EasyChair |