KIT | KIT-Bibliothek | Impressum | Datenschutz

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

Wasserrab, Daniel

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.



Zugehörige Institution(en) am KIT Institut für Programmstrukturen und Datenorganisation (IPD)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Zeitschriftenaufsatz
Publikationsjahr 2009
Sprache Englisch
Identifikator ISSN: 2150-914X
KITopen-ID: 1000017685
Erschienen in The Archive of Formal Proofs
Heft 11
Seiten 543 S.
Projektinformation KASTEL I (BMBF, 01BY1172 / 16BY1172)
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page