logo SBA

ETD

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

Tesi etd-07022019-195342


Tipo di tesi
Tesi di laurea magistrale
Autore
MAZZONI, MICHELE
URN
etd-07022019-195342
Titolo
An efficient abstract domain for the approximation of machine integers
Dipartimento
INFORMATICA
Corso di studi
INFORMATICA
Relatori
relatore Prof.ssa Gori, Roberta
relatore Prof. Bagnara, Roberto
Parole chiave
  • software verification
  • c++
  • static analysis
  • abstract interpretation
Data inizio appello
26/07/2019
Consultabilità
Non consultabile
Data di rilascio
26/07/2089
Riassunto
Software verification is essential for building reliable systems, but it requires well-crafted tools whose development is a non-trivial task.
This thesis presents an abstract domain based on multi-intervals for the approximation of machine integers and arithmetic, logic and bitwise operations over them.
The C++ implementation of the abstract domain has been carefully engineered for maximum efficiency, both in terms of memory occupation and of execution time.
The applications of this abstract domain range from static analysis, to symbolic model-checking, to constraint-based generation of test cases.
File