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.

翻译：大多数用于分离逻辑的自动程序验证器采用符号执行或验证条件生成技术来提取证明义务，随后将这些义务交由SMT求解器处理。现有的验证算法设计均注重可靠性，但在性能和完备性方面存在差异。这些特性也可能因待验证的程序和属性而异。因此，程序验证器的开发者和使用者必须针对其应用领域谨慎选择验证算法。要做出明智决策，需要对现代分离逻辑验证器所用验证算法的性能与完备性特征进行系统比较，然而此类比较目前尚属空白。本文阐述了五种分离逻辑验证算法，其中三种为现有工具所采用，另两种新颖算法融合了现有符号执行与验证条件生成算法的特性。通过在Viper基础设施中对这五种算法实现进行详细评估，本文考察了它们在不同类型输入程序上的性能与完备性表现。基于实验结果，我们提出了能最大化完备性与性能的候选算法组合方案。