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 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. © 2008 Springer Berlin Heidelberg.
CITATION STYLE
Wasserrab, D., & Lochbihler, A. (2008). Formalizing a framework for dynamic slicing of program dependence graphs in Isabelle/HOL. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5170 LNCS, pp. 294–309). Springer Verlag. https://doi.org/10.1007/978-3-540-71067-7_24
Mendeley helps you to discover research relevant for your work.