Search arXiv⌕ Search
Home/Archive/arXiv

arXiv · 1401.6227

From Safety To Termination And Back: SMT-Based Verification For Lazy Languages

Niki Vazou·Eric L. Seidel·Ranjit Jhala
View original source ↗Read source document ↗Export metadata ↓

Abstract

SMT-based verifiers have long been an effective means of ensuring safety properties of programs. While these techniques are well understood, we show that they implicitly require eager semantics; directly applying them to a lazy language is unsound due to the presence of divergent sub-computations. We recover soundness by composing the safety analysis with a termination analysis. Of course, termination is itself a challenging problem, but we show how the safety analysis can be used to ensure termination, thereby bootstrapping soundness for the entire system. Thus, while safety invariants have long been required to prove termination, we show how termination proofs can be to soundly establish safety. We have implemented our approach in liquidHaskell, a Refinement Type-based verifier for Haskell. We demonstrate its effectiveness via an experimental evaluation using liquidHaskell to verify safety, functional correctness and termination properties of real-world Haskell libraries, totaling over 10,000 lines of code.

Explore related subjects

cs.PL

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Niki Vazou, Eric L. Seidel, Ranjit Jhala. 2014-01-24. From Safety To Termination And Back: SMT-Based Verification For Lazy Languages. https://arxiv.org/abs/1401.6227

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Schedules Are Solvable Symbols: Tuning-Free Compilation of Tile Programs on Dataflow Architectures

Modern AI and HPC accelerators increasingly expose dataflow features: software-visible mechanisms for data movement and overlap, such as inter-core communication through the on-chip network and intra-core asynchronous pipelining. These features shift scheduling responsibility from hardware to the compiler, and because placement, movement, and synchronization become software-visible, they also make the performance of static schedules predictable. Yet high performance on such hardware still relies on vendor-engineered kernel libraries or profile-based auto-tuning, whose embedded expert knowledge transfers poorly across architectures and algorithms. We present Loom, a tuning-free symbolic compiler framework for tile-based SPMD programs on spatial dataflow architectures. The central idea is to treat tile-based SPMD compilation as a hardware-explicit static optimization problem. Loom enumerates discrete spatial-mapping and communication candidates while keeping value parameters, such as tiling factors and pipeline knobs, symbolic within each candidate. From an explicit hardware description, it derives symbolic legality constraints and latency expressions, formulates one CP-SAT problem per schedule candidate, and jointly solves inter-core dataflow, intra-core asynchronous scheduling, and block sizes at compile time. On two Tenstorrent generations, Wormhole and Blackhole, Loom matches or exceeds the vendor-optimized TTNN library on GEMM, Flash Attention, and Flash Decode, out of the box and without per-shape profiling or profile-based platform-specific schedule tuning. These results suggest that hardware-derived symbolic compilation provides a retargetable alternative to profiling-based tuning for spatial dataflow architectures while remaining interpretable by keeping optimization decisions traceable to source-level symbols.

cs.PL↗
arXiv2026

ProofGap: Benchmarking Step-Level Formal Reasoning with Local Obligations Derived from Natural-Language Solutions

Existing formal mathematics benchmarks, such as miniF2F, ProofNet, and PutnamBench, primarily evaluate models on constructing complete formal proofs for challenging problems. Because success is measured at the theorem level, these benchmarks offer limited insight into models' step-level formal reasoning. Evaluating this capability separately enables finer-grained diagnosis of model limitations than theorem-level evaluation alone. To fill this evaluation gap, we introduce ProofGap, a fine-grained benchmark for step-level formal reasoning. ProofGap is constructed through a natural-language proof-processing pipeline that decomposes each reasoning step into one or more aligned proof gaps. Applying this pipeline to natural-language solutions to 3,015 exercises in B. P. Demidovich's Problems in Mathematical Analysis yields 26,116 gaps. The benchmark focuses on mathematical analysis, a domain that remains challenging for current models. By supplying the local context and target explicitly, gap completion isolates local formal proof construction from end-to-end proof composition, enabling more precise localization of model failures. Natural-language solutions serve as the provenance of these obligations, while the benchmark task itself starts from an already formalized local context and goal. Beyond benchmarking, the same pipeline may support future proof-verification systems, provided that semantic translation and sequential proof composition are handled reliably.

cs.PL↗
arXiv2026

Sound State Encodings in Translational Separation Logic Verifiers (Extended Version)

Automated program verifiers are often organized into a front-end, which encodes an input program into an intermediate verification language (IVL), and a back-end, which proves that the IVL program is correct. Soundness of such translational verifiers requires that the back-end verification is sound and that correctness of the IVL program implies correctness of the input program. Existing formalizations for translational verifiers based on separation logic target the former, but support the latter only under the strong assumption that there exists a separation logic for the input program with the same state model as the IVL. This assumption is unrealistic in practice, especially since the state model also defines the supported separation logic resources. We present the first formal framework for proving the soundness of translational separation logic verifiers with non-trivial state encodings. To be applicable to various front-ends and IVLs, our framework only assumes the existence of a homomorphic encoding relation between the front-end and IVL state models. At the core of our framework is a novel condition, backward satisfiability, which is crucial to guarantee the soundness of the front-end translation. We formalize our framework for front-end verifiers based on concurrent separation logic and separation logic IVLs, such as Raven, VeriFast, and Viper. We demonstrate its expressiveness by proving soundness for three common state encodings. Our framework and all proofs are formalized in Isabelle/HOL.

cs.PL↗