Backing up Slicing : Verifying the Interprocedural Two-Phase Horwitz-Reps-Binkley Slicer
Daniel Wasserrab · 2009
Slicing is a widely-used technique with applications in e.g. compiler technology and software security. Thus verification of algorithms in these areas is often based on the correctness of slicing, which should ideally be proven independent of concrete programming languages and with the help of well-known verifying techniques such as proof assistants. After verifying static intraprocedural and dynamic slicing [3], we focus now on the sophisticated interprocedural two-phase Horwitz-Reps-Binkley slicer [1], including summary edges which were added in [2]. Again, abstracting from concrete syntax we base our work on a graph representation of the program fulfilling certain structural and well-formedness properties. The framework is instantiated with a simple While language with procedures, showing its validity. 0.1 Auxiliary lemmas theory AuxLemmas imports Main begin Lemma concerning maps and @ lemma map-append-append-maps: assumes map:map f xs =