### Abstract

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. As a first step in this direction, this contribution presents a framework for dynamic and static intraprocedural slicing based on control flow and program dependence graphs. Abstracting from concrete syntax we base the framework on a graph representation of the program fulfilling certain structural and well-formedness properties.
The formalization consists of the basic framework (in subdirectory Basic/), the correctness proof for dynamic slicing (in subdirectory Dynamic/), the correctness proof for static intraprocedural slicing (in subdirectory StaticIntra/) and instantiations of the framework with a simple While language (in subdirectory While/) and the sophisticated object-oriented bytecode language of Jinja (in subdirectory JinjaVM/). For more information on the framework, see the TPHOLS 2008 paper by Wasserrab and Lochbihler and the PLAS 2009 paper by Wasserrab et al.

### License

BSD License

### Topics

- Computer science/Programming languages/Static analysis

### Session Slicing

- AuxLemmas
- BasicDefs
- CFG
- CFGExit
- Postdomination
- CFG_wf
- CFGExit_wf
- SemanticsCFG
- DynDataDependence
- DynStandardControlDependence
- DynWeakControlDependence
- DynPDG
- DependentLiveVariables
- BitVector
- DynSlice
- Observable
- Distance
- DataDependence
- Slice
- StandardControlDependence
- WeakControlDependence
- PDG
- WeakOrderDependence
- CDepInstantiations
- ControlDependenceRelations
- Com
- WCFG
- Interpretation
- Labels
- WellFormed
- AdditionalLemmas
- DynamicControlDependences
- Semantics
- WEquivalence
- SemanticsWellFormed
- StaticControlDependences
- JVMCFG
- JVMInterpretation
- JVMPostdomination
- JVMCFG_wf
- JVMControlDependences
- SemanticsWF
- Slicing

### Depends on

- Jinja is not Java

### Used by

- Verified Construction of Static Single Assignment Form
- Information Flow Noninterference via Slicing

### Auto-related entries

- Information Flow Control via Dependency Tracking

## Cite

×

Slicing-AFP

    @article{Slicing-AFP,
      author  = {Daniel Wasserrab},
      title   = {Towards Certified Slicing},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2008},
      note    = {\url{https://isa-afp.org/entries/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 20, 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
- Apr 30, 2009 : Isabelle2009
- Apr 29, 2009 : Isabelle2009
- Sep 22, 2008 : Isabelle2008