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.
Type de document :
Pré-publication, Document de travail
Liste complète des métadonnées
Contributeur : Alain Monteil <>
Soumis le : jeudi 14 janvier 2016 - 16:21:31
Dernière modification le : vendredi 25 mai 2018 - 12:02:07

Lien texte intégral


  • 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〉



Consultations de la notice