Email Gateway (Aug 18 2022 at 14:20): Email Gateway (Aug 18 2022 at 14:20):From: Tobias Nipkow <nipkow@in.tum.de>
http://afp.sourceforge.net/entries/HRB-Slicing.shtml
Backing up Slicing: Verifying the Interprocedural Two-Phase
Horwitz-Reps-Binkley Slicer
Author: Daniel Wasserrab
Abstract: After verifying dynamic and static interprocedural slicing, we
present a modular framework for static interprocedural slicing. To this
end, we formalized the standard two-phase slicer from Horwitz, Reps and
Binkley (see their TOPLAS 12(1) 1990 paper) together with summary edges
as presented by Reps et al. (see FSE 1994). The framework is again
modular in the programming language by using an abstract CFG, defined
via structural and well-formedness properties. Using a weak simulation
between the original and sliced graph, we were able to prove the
correctness of static interprocedural slicing. We also instantiate our
framework with a simple While language with procedures. This shows that
the chosen abstractions are indeed valid.
Enjoy!
Tobias
Email Gateway (Aug 18 2022 at 14:20):From: Jens Doll <jd@cococo.de>
The corresponding paper >proof outline< is a little confusing to me,
because it contains the machine readable sources.
Was it meant to be read or to be processed?
Jens
P.S.: the same applies to >proof theory<
Email Gateway (Aug 18 2022 at 14:20):From: Tobias Nipkow <nipkow@in.tum.de>
This is an Isabelle feature not a bug. Thy files are processed, as a
side effect tex files are produced and turned into pdf, which is meant
to be read. For example to get an overview that hides the proofs.
Tobias
Jens Doll wrote:
Last updated: Apr 20 2024 at 01:05 UTC