Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Verification Algorithms for Automated Separation Logic Verifiers

Marco Eilers, Malte Schwerhoff, Peter Müller

TL;DR

This paper tackles the problem of selecting effective verification algorithms for separation-logic verifiers by implementing and evaluating five algorithms (three existing and two novel SE variants) within the Viper framework. It systematically compares their completeness and performance across a large, diverse benchmark set, revealing that partial-heap SE algorithms (notably SE-PS) typically offer best overall completeness and speed, while total-heap strategies excel on branch-heavy inputs. The authors also introduce two novel SE variants (SE-TR and SE-PC) that blend SE with total-heap techniques, and demonstrate that carefully designed portfolios of algorithms substantially improve robustness and coverage. The results support adopting multi-algorithm portfolios tailored to input characteristics, offering practical guidance for building more reliable and performant separation-logic verifiers.

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.

Verification Algorithms for Automated Separation Logic Verifiers

TL;DR

This paper tackles the problem of selecting effective verification algorithms for separation-logic verifiers by implementing and evaluating five algorithms (three existing and two novel SE variants) within the Viper framework. It systematically compares their completeness and performance across a large, diverse benchmark set, revealing that partial-heap SE algorithms (notably SE-PS) typically offer best overall completeness and speed, while total-heap strategies excel on branch-heavy inputs. The authors also introduce two novel SE variants (SE-TR and SE-PC) that blend SE with total-heap techniques, and demonstrate that carefully designed portfolios of algorithms substantially improve robustness and coverage. The results support adopting multi-algorithm portfolios tailored to input characteristics, offering practical guidance for building more reliable and performant separation-logic verifiers.

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.
Paper Structure (39 sections, 4 figures, 1 table)

This paper contains 39 sections, 4 figures, 1 table.

Table of Contents

  1. Introduction
  2. This Work.
  3. Contributions and Outline.
  4. Verification Algorithms
  5. Viper Verification Language
  6. Design Dimensions
  7. SE vs. VCG.
  8. Partial vs. Total Heaps.
  9. Algorithms
  10. SE-PS.
  11. SE-PC.
  12. SE-TR.
  13. VCG-TR.
  14. VCG-TA.
  15. Evaluation
  16. ...and 24 more sections

Figures (4)

  • Figure 1: Box plot of relative percentage difference (RPD) of mean performance per group for the two extreme points in the design space, SE-PS vs. VCG-TA. Values greater than zero indicate that the first algorithm in the pair is faster, values less than zero that the second is faster; the orange line denotes the median and the dashed green line the mean.
  • Figure 2: Box plots of relative percentage difference (RPD) of mean performance per group. From top to bottom: (a) SE-PS vs. SE-PC, (b) SE-PS vs. SE-TR, (c) SE-TR vs. VCG-TR, (d) VCG-TR vs. VCG-TA. As before, values greater than zero indicate that the first algorithm in the pair is faster, values less than zero that the second is faster. The orange line denotes the median, the dashed green line the mean.
  • Figure 3: Box plots of relative percentage difference (RPD) of mean performance for pairs of portfolios. From top to bottom: a) $P0$ vs. $P1$, b) $P0$ vs. $P2$, c) $P0$ vs. $P3$.
  • Figure 4: Box plots of relative percentage difference (RPD) of mean performance comparing SE-PS to different portfolios. From top to bottom: a) SE-PS vs. $P1$, b) SE-PS vs. $P2$, c) SE-PS vs. $P3$.