Synthesizing Short-Circuiting Validation of Data Structure Invariants

Yi-Fan Tsai, Devin Coughlin, Bor-Yuh Evan Chang +1

This paper presents incremental verification-validation, a novel approach for checking rich data structure invariants expressed as separation logic assertions. Incremental verifica…