Email Gateway (Aug 18 2022 at 12:26): Email Gateway (Aug 18 2022 at 12:26):From: Lawrence Paulson <lp15@cam.ac.uk>
Many thanks to Daniel Wasserrab for his contribution to the Archive of
Formal Proofs, http://afp.sourceforge.net/, entitled "Towards
Certified Slicing". Abstract appears below.
Larry Paulson
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 an instantiation of the framework
with a simple While language (in subdirectory While/). For more
information on the framework and dynamic slicing, see the TPHOLS 2008
paper by Wasserrab and Lochbihler.
Last updated: Nov 21 2024 at 12:39 UTC