Gradual Verification: Assuring Software Incrementally

By: Jonathan Aldrich

Abstract

Current static verification techniques do not provide good support for incrementality, making it difficult for developers to focus on specifying and verifying the properties and components that are most important. Dynamic verification approaches support incrementality, but cannot provide static guarantees. To bridge this gap, we propose gradual verification, which supports incrementality by allowing every assertion to be complete, partial, or omitted, and provides sound verification that smoothly scales from dynamic to static checking.

Keywords

Gradual verification, Dynamic and static checking, Program specification, Soundness

Cite as:

Jonathan Aldrich, “Gradual Verification: Assuring Software Incrementally”, Journal of Object Technology, Volume 25, no. 1 ( 2026), pp. 1:1-1, doi:10.5381/jot.2026.25.1.a1.

DOI | BiBTeX | Tweet this | Post to CiteULike | Share on LinkedIn