  Most automated program verifiers for separation logic use either symbolic
execution or verification condition generation to extract proof obligations,
which are then handed over to an SMT solver. Existing verification algorithms
are designed to be sound, but differ in performance and completeness. These
characteristics may also depend on the programs and properties to be verified.
Consequently, developers and users of program verifiers have to select a
verification algorithm carefully for their application domain. Taking an
informed decision requires a systematic comparison of the performance and
completeness characteristics of the verification algorithms used by modern
separation logic verifiers, but such a comparison does not exist.
  This paper describes five verification algorithms for separation logic, three
that are used in existing tools and two novel algorithms that combine
characteristics of existing symbolic execution and verification condition
generation algorithms. A detailed evaluation of implementations of these five
algorithms in the Viper infrastructure assesses their performance and
completeness for different classes of input programs. Based on the experimental
results, we identify candidate portfolios of algorithms that maximize
completeness and performance.
