Sciweavers

Share
TPHOL
2008
IEEE

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

9 years 4 months ago
Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in Isabelle/HOL
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 slicing based on control flow and 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.
Daniel Wasserrab, Andreas Lochbihler
Added 01 Jun 2010
Updated 01 Jun 2010
Type Conference
Year 2008
Where TPHOL
Authors Daniel Wasserrab, Andreas Lochbihler
Comments (0)
books