### 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.

### License

BSD License

### Topics

- Computer science/Programming languages/Static analysis

### Session HRB-Slicing

- AuxLemmas
- BasicDefs
- CFG
- CFGExit
- CFG_wf
- CFGExit_wf
- SemanticsCFG
- ReturnAndCallNodes
- Observable
- Postdomination
- SDG
- HRBSlice
- SCDObservable
- Distance
- Slice
- WeakSimulation
- FundamentalProperty
- Com
- ProcState
- PCFG
- WellFormProgs
- Interpretation
- Labels
- WellFormed
- ValidPaths
- ProcSDG
- JVMCFG
- JVMInterpretation
- JVMCFG_wf
- JVMPostdomination
- JVMSDG
- HRBSlicing

### Depends on

- Jinja is not Java

### Used by

- Inter-Procedural Information Flow Noninterference via Slicing

## Cite

×

HRB-Slicing-AFP

    @article{HRB-Slicing-AFP,
      author  = {Daniel Wasserrab},
      title   = {Backing up Slicing: Verifying the Interprocedural Two-Phase Horwitz-Reps-Binkley Slicer},
      journal = {Archive of Formal Proofs},
      month   = {November},
      year    = {2009},
      note    = {\url{https://isa-afp.org/entries/HRB-Slicing.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Feb 16, 2013 : Isabelle2013
- May 24, 2012 : Isabelle2012
- Oct 11, 2011 : Isabelle2011-1
- Feb 11, 2011 : Isabelle2011
- Jul 1, 2010 : Isabelle2009-2
- Dec 12, 2009 : Isabelle2009-1
- Nov 19, 2009 : Isabelle2009