Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Synthesizing Short-Circuiting Validation of Data Structure Invariants

Abstract : This paper presents incremental verification-validation, a novel approach for checking rich data structure invariants expressed as separation logic assertions. Incremental verification-validation combines static verification of separation properties with efficient, short-circuiting dynamic validation of arbitrarily rich data constraints. A data structure invariant checker is an inductive predicate in separation logic with an executable interpretation; a short-circuiting checker is an invariant checker that stops checking whenever it detects at run time that an assertion for some sub-structure has been fully proven statically. At a high level, our approach does two things: it statically proves the separation properties of data structure invariants using a static shape analysis in a standard way but then leverages this proof in a novel manner to synthesize short-circuiting dynamic validation of the data properties. As a consequence, we enable dynamic validation to make up for imprecision in sound static analysis while simultaneously leveraging the static verification to make the remaining dynamic validation efficient. We show empirically that short-circuiting can yield asymptotic improvements in dynamic validation, with low overhead over no validation, even in cases where static verification is incomplete.
Document type :
Preprints, Working Papers, ...
Complete list of metadata
Contributor : Alain Monteil Connect in order to contact the contributor
Submitted on : Thursday, January 14, 2016 - 4:21:31 PM
Last modification on : Thursday, March 17, 2022 - 10:08:44 AM

Links full text


  • HAL Id : hal-01256324, version 1
  • ARXIV : 1511.04846



Yi-Fan Tsai, Devin Coughlin, Bor-Yuh Evan Chang, Xavier Rival. Synthesizing Short-Circuiting Validation of Data Structure Invariants. 2015. ⟨hal-01256324⟩



Record views