KIT | KIT-Bibliothek | Impressum | Datenschutz

Towards Certified Slicing

Wasserrab, Daniel

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 and ... mehr


Zugehörige Institution(en) am KIT Institut für Programmstrukturen und Datenorganisation (IPD)
Publikationstyp Zeitschriftenaufsatz
Jahr 2008
Sprache Englisch
Identifikator ISSN: 2150-914X
KITopen ID: 1000017686
Erschienen in The Archive of Formal Proofs
Heft 9
Seiten 326 S.
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page