Gradually Verifying Unfolding Expressions & Pure Functions

Hazel Torek Long Nguyen Priyam Gupta Jenna DiVincenzo Jonathan Aldrich

Jul 2026 · arXiv.org · Vol abs/2607.15383 · 0 citations

Computer Science

TL;DR

This paper presents the formal semantics for unfolding expressions and pure functions for a static verifier using symbolic execution, extend it for a gradual verifier, and provides a proof of soundness.

Abstract

Unfolding expressions, which temporarily unfold a predicate to leverage its owned fields when evaluating a heap-dependent expression, and pure functions, which are heap-dependent functions that can be used in specifications, are used in deductive program verifiers based on implicit dynamic frames, such as Gradual C0, Gobra, Nagini, and SnaKt, to increase the modularity of specifications involving ownership. In this paper, we present the formal semantics for unfolding expressions and pure functions for a static verifier using symbolic execution, extend it for a gradual verifier, and provide a proof of soundness. To support Gradual C0, our proof is in the setting of gradual verification, a deductive program verification system that combines static and dynamic verification to allow partial specifications. However, because the gradual verifier is a conservative extension of a static verifier, our results also apply to static verifiers that use symbolic execution, such as the Silicon symbolic execution backend for the Viper verification infrastructure used by Gobra, Nagini, and SnaKt.

DOI arXiv Semantic Scholar

View source

Similar papers

2026

Lazy Proof Automation for Separation Logic

The key idea is to implement an entailment checker as a combination of an efficient but unverified prover, suitable for fast-paced interactive proofs, and a proof reconstruction procedure that takes the prover’s trace and produces a certificate of entailment validity that can be checked a posteriori.

V. Mikhal'chuk, V. Gladshtein, I. Sergey · International Conference on... · 0 citations

Preprint Aug 2026

Towards a Deductive Verification Infrastructure for Weighted Programming

This work presents a deductive verification framework based on a weighted assertion language and an intermediate verification language, whose weight domains are ordered structures with implication and coimplication, which let verification conditions express lower- and upper-bound obligations internally.

Emma Ahrens, Samuel Rode, Philipp Schröer et al. · 0 citations

Preprint Aug 2026

Synchronous Observers Revisited for Runtime Verification of Lustre Using STL

This work presents a technique for compiling the synchronous fragment of STL (SSTL) into synchronous observers in the dataflow language Lustre, and contributes an interactive visualiser that renders a property's three-valued verdict over an editable trace.

Logan Kenwright, Partha S. Roop, Sobhan Chatterjee et al. · 0 citations

Open access Aug 2026

Assertions for Free: Transferring Invariants from Algorithm to Implementation Proofs (Functional Pearl)

This pearl shows how a clean separation can be achieved within the two-layer method by combining two simple ideas: expressing implementation correctness as a relational Hoare quadruple, and introducing assertion annotations into the abstract program to capture key invariants.

Shu-Shu Wu, Cheng-Xi Yang, Xi-Wei Wu et al. · Proc. ACM Program. Lang. · 0 citations

A Compilation-based Under-Constrained Execution Engine

Mingjun Yin, Zhao-Rui Li, Ju Chen et al. · 0 citations

Preprint Aug 2026

Circuit-Based Program Verification: Sequential Circuits as an Intermediate Representation for Verifying C Programs

Circuit-Based Program Verification is presented, a modular framework that translates C programs into sequential circuits and employs off-the-shelf hardware model checkers as backends and integrates multiple state-of-the-art hardware model checkers, which together provide access to diverse verification algorithms.

Po-Chun Chien, Nian-Ze Lee, Armin Biere et al. · 0 citations