We submit an artifact with all the software needed to reproduce our experiments. Based on a number of benchmarks, including the running examples from our paper, we demonstrate how the claimed classes of programs (methods with relatively convex DAG or ZOPG footprints) can be systematically translated into the Viper verification language and verified using one of Viper’s standard verification backends. Our experiments confirm the precision claims of the paper by demonstrating that examples with precise structural invariants (that specify reachability and unreachability at the same time) can be encoded and verified in our technique. Beyond successful verification attempts, we show that bugs in the implementation and the specification of such programs are also efficiently detected by the tool. Additionally, our experiments support the following claims from the paper:

• The complicated quantifiers employed for reachability framing, local updates, checking acyclicity, etc. are hidden from the user (in our examples, these are encapsulated in macros, representing the systematic steps of our encoding). Note that, since the preliminary version of the paper, we improved the encoding such that manual assertions (previously mentioned in the evaluation) beyond those generated systematically are no-longer needed
• Our technique allows the user to efficiently combine reachability predicates over different sets of reference fields.
• Specifications of conceptually different properties in our technique do not result in entangled proof obligations and can be verified independently.