Verification Algorithms for Automated Separation Logic Verifiers

TL;DR

This paper systematically compares five verification algorithms for separation logic, evaluating their performance and completeness to guide better algorithm selection in automated program verification tools.

Contribution

It introduces two novel algorithms combining symbolic execution and verification condition generation, and provides a comprehensive empirical comparison of five algorithms.

Findings

Identifies algorithms with optimal performance for different program classes

Provides a portfolio of algorithms balancing completeness and efficiency

Highlights trade-offs between existing verification techniques

Abstract

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.