ETD

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

Tesi etd-06042021-215435


Tipo di tesi
Tesi di laurea magistrale
Autore
MANINI, NICOLAS
URN
etd-06042021-215435
Titolo
Deciding program properties via complete abstractions on bounded domains
Dipartimento
INFORMATICA
Corso di studi
INFORMATICA
Relatori
relatore Prof. Bruni, Roberto
relatore Prof.ssa Gori, Roberta
Parole chiave
  • abstract interpretation
  • complete abstract domains
  • bounded domains
  • program termination
  • decidability
  • program equivalence
  • language expressiveness
Data inizio appello
25/06/2021
Consultabilità
Non consultabile
Data di rilascio
25/06/2024
Riassunto
Abstract interpretation is very useful for program analysis, because it provides a (sound) over-approximation of program behaviours.
When such approximation is as precise as possible in the current abstract domain, we say the analysis is complete, which is the best possible scenario for the analysis.
Unfortunately it has been shown that whenever the programming language is Turing equivalent, then only trivial abstract domains are complete for all programs.

Therefore, given a non-trivial abstract domain, we want to characterize the classes of complete programs on that domain and which is the expressiveness of such complete programs.
To this aim, in this thesis we introduce the notion of bounded domains to denote posets admitting ascending chains of bounded length only and restrict our attention to investigate the expressiveness of programs for which the analysis is complete.

The first result is that any complete program on bounded domains can be rewritten in an equivalent canonical form without nontrivial loops.
This result enables us to conclude that program termination is decidable and gives an effective approach to solve it.

As a second result, we show that the semantic equivalence between any two programs can be reduced to determining equivalence between sets of guarded statements.
File