logo SBA

ETD

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

Tesi etd-07022021-105407


Tipo di tesi
Tesi di laurea magistrale
Autore
ASCARI, FLAVIO
URN
etd-07022021-105407
Titolo
Limits and difficulties in designing under-approximation abstract domains
Dipartimento
INFORMATICA
Corso di studi
INFORMATICA
Relatori
relatore Bruni, Roberto
relatore Gori, Roberta
Parole chiave
  • abstract domain
  • abstract interpretation
  • under-approximation
Data inizio appello
23/07/2021
Consultabilità
Completa
Riassunto
Static program analyses are a set of useful techniques that allows to infer properties on programs from their source code, without executing them. Among those, abstract interpretation is a general framework to define sound analyses based on constructive approximations that found its way through many aspects of modern Computer Science.
Nowadays most formal static analyses focus on over-approximation, that is they determine a set bigger than the set of all possible behaviours of the program, in order to show absence of bugs: if the analysis reports no unwanted behaviour, then the program doesn't have any.
In principle there is another, dual application of static analyses: to compute and under-approximation of the set of possible behaviours in order to find bugs. However, this kind of analyses hasn't been studied as intensively as over-approximations in the last few decades, and even though abstract interpretation has been proposed for over as well as under-approximation, in practice has almost only been used for the former.

In this thesis, we would like to investigate both technical and conceptual reasons that make the design of under-approximation abstract domains difficult. We present the main differences between over and under-approximation, and we propose the new definition of ``non emptying function" to describe a function whose analysis produces a non vacuous result. Using this definition, we give conditions for the non existence of under-approximation domains. Lastly, we study the limitations of approaches that use this definition in order to prove non existence of such domains.
File