Data Structure Abstraction and Incorrectness Separation Logic
summary
Extends incorrectness separation logic to support data-structure abstraction (lists, sets) and reports a mostly complete Rock mechanization. Shows standard ISL spec lets list→list abstraction validate but fails for list→set because universal reachability requires all heap models to be executable. Proposes weakening that quantification to an existential frame-compatible representative, partitioning post-state space so realistic implementations become reachable. Prototype reasoning thus becomes valid for the harder examples; work remains ongoing.
AI-written summary · about
related talks
21mOutcome Separation Logic: Local Reasoning for Correctness and Incorrectness with(…)
19mSystem-level weak memory models: The need for formalisation, ISA semantics integ...
25mA Logic for the Imprecision of Abstract Interpretations
26mA Rule-Based Approach for Designing and Composing Abstract Domains
22mImplementing separation logic using an SMT-backed Frame Rule
24mThe Best of Abstract Interpretations
32mA mechanised and constructive reverse analysis of soundness and completeness of b...
05mNew foundations for probabilistic separation logic