### Introduction

Reasoning about memory aliasing and mutation in software verification is a hard problem. Linear (ownership) types make it much easier in practice.

### Abstract

Reasoning about memory aliasing and mutation in software verification is a hard problem. This is especially
true for systems using SMT-based automated theorem provers. Memory reasoning in SMT verification typically
requires a nontrivial amount of manual effort to specify heap invariants, as well as extensive alias reasoning
from the SMT solver. In this paper, we present a hybrid approach that combines linear types with SMT-based
verification for memory reasoning. We integrate linear types into Dafny, a verification language with an SMT
backend, and show that the two approaches complement each other. By separating memory reasoning from
verification conditions, linear types reduce the SMT solving time. At the same time, the expressiveness of SMT
queries extends the flexibility of the linear type system. In particular, it allows our linear type system to easily
and correctly mix linear and nonlinear data in novel ways, encapsulating linear data inside nonlinear data and
vice-versa. We formalize the core of our extensions, prove soundness, and provide algorithms for linear type
checking. We evaluate our approach by converting the implementation of a verified storage system (~24K
lines of code and proof) written in Dafny, to use our extended Dafny. The resulting system uses linear types
for 91% of the code and SMT-based heap reasoning for the remaining 9%. We show that the converted system
has 28% fewer lines of proofs and 30% shorter verification time overall. We discuss the development overhead
in the original system due to SMT-based heap reasoning and highlight the improved developer experience
when using linear types.