HOME | DEUTSCH | IMPRESSUM | KIT

Conference Papers: Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL

[wasserrab08tphols]Daniel Wasserrab, Andreas Lochbihler, Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL, Outmane Ait Mohamed and César Muñoz and Sofiène Tahar (Ed.), Proceedings of the 21st International Conference of Theorem Proving in Higher Order Logics, pp. 294--309, Springer, Montréal, Québec, Canada, August 2008.

Abstract

Slicing is a widely-used technique with applications in e.g. compiler technology, debugging 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 theorem provers. As a first step in this direction, this contribution presents a framework for dynamic slicing, based on control flow and program dependence graphs and machine checked in Isabelle/HOL. Abstracting from concrete syntax we base the framework on a graph representation of the program fulfilling certain structural and well-formedness properties.

Download

  [PDF]   [DOI]

Original article available at springerlink.com.

BibTeX

Authors at the institute

Former Staff Member
Dr. rer. nat. Andreas Lochbihler
Dr.-Ing. Daniel Wasserrab

Projects

Project
Quis-Custodiet