logo SBA

ETD

Archivio digitale delle tesi discusse presso l’Università di Pisa

Tesi etd-10292022-123601


Tipo di tesi
Tesi di laurea magistrale
Autore
PIAZZESI, NICCOLO'
URN
etd-10292022-123601
Titolo
Local Completeness Logic on strategic term rewriting
Dipartimento
INFORMATICA
Corso di studi
INFORMATICA
Relatori
relatore Bruni, Roberto
Parole chiave
  • abstract interpretation
  • formal methods
  • term rewriting
Data inizio appello
02/12/2022
Consultabilità
Tesi non consultabile
Riassunto
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.
File