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

TL;DR

This paper presents a novel SMT-based verification approach for lazy languages that combines safety and termination analysis to ensure soundness, implemented in liquidHaskell and validated on real-world Haskell code.

Contribution

It introduces a method to achieve sound verification in lazy languages by composing safety and termination analyses, overcoming the limitations of existing eager semantics-based techniques.

Findings

Successfully verified safety, correctness, and termination of large Haskell libraries

Demonstrated the approach's effectiveness on over 10,000 lines of real-world code

Bootstrapped safety and termination proofs to ensure soundness in lazy language verification

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.