An Automatic Encoding from VeriFast Predicates into Implicit Dynamic Frames

Abstract

VeriFast is a symbolic-execution-based verifier, based on separation logic specifications. Chalice is a verifier based on verification condition generation, which employs specifications in implicit dynamic frames. Recently, theoretical work has shown how the cores of these two verification logics can be formally related. However, the mechanisms for abstraction in the two tools are not obviously comparable; VeriFast employs parameterised recursive predicates in specifications, while Chalice employs recursive predicates without parameters, along with heap-dependent abstraction functions.

In this paper, we show how to relate a subset of VeriFast, including many common uses of separation logic recursive predicates, to the implicit dynamic frames approach. In particular, we present a prototype tool which can translate a class of VeriFast examples into Chalice examples. Our tool performs several semantic analyses of predicate definitions, and determines which of a selection of novel techniques can be applied to infer appropriate predicate and function definitions, as well as corresponding code instrumentation in a generated program. The tool is automatic, and produces programs which can themselves be directly handled by the automatic Boogie/Z3-based Chalice verifier.