• formal methods
• term rewriting
• abstract interpretation

In Abstract Interpretation, completeness is an ideal situation in which the
abstraction does not introduce any false alerts. Completeness is notoriously
difficult to achieve in practice, because it is a global property: it must hold
for any possible input. The weakened notion of local completeness relaxes
this requirement by considering only some specific inputs, finding wider
applicability in practice. Local Completeness Logic (LCL) is a novel proof
system that can reason about both correctness and incorrectness of locally
complete computations, by combining over and under-approximating static
analysis. In this thesis, we study the applicability of the LCL framework
to the context of strategic rewriting, where the classical notion of term
rewriting is enriched by the definition of strategies, whose purpose is to
guide and control the application of rules. We present a new strategy lan-
guage, Strat, and extend the LCL proof system to reason about properties
of Strat programs.