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基础设施中实现这五种算法，并针对不同类别的输入程序进行详细评估，我们考察了它们的性能和完备性。基于实验结果，我们确定了能够最大化完备性和性能的候选算法组合。