[isabelle] New AFP entry: Verifying the Interprocedural Two-Phase Horwitz-Reps-Binkley Slicer


Backing up Slicing: Verifying the Interprocedural Two-Phase
Horwitz-Reps-Binkley Slicer

Author: Daniel Wasserrab

Abstract: After verifying dynamic and static interprocedural slicing, we
present a modular framework for static interprocedural slicing. To this
end, we formalized the standard two-phase slicer from Horwitz, Reps and
Binkley (see their TOPLAS 12(1) 1990 paper) together with summary edges
as presented by Reps et al. (see FSE 1994). The framework is again
modular in the programming language by using an abstract CFG, defined
via structural and well-formedness properties. Using a weak simulation
between the original and sliced graph, we were able to prove the
correctness of static interprocedural slicing. We also instantiate our
framework with a simple While language with procedures. This shows that
the chosen abstractions are indeed valid.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.