Update title

chapters/5-Encoding.typ

@@ -1,2 +1,6 @@
 #pagebreak(to:"odd")
 = Encoding in Viper
+== Classes Encoding
+== Functions Encoding
+== Function Calls Encoding
+== Predicates Unfolding

config/variables.typ

@@ -2,7 +2,7 @@
 #let myLang = "en"
 #let myName = "Francesco Protopapa"
 #let myMatricola = "2079466"
-#let myTitle = "Using uniqueness annotations to formally verify Kotlin code with Viper"
+#let myTitle = "Controlling uniqueness to formally verify Kotlin code with Viper"
 #let myDegree = "Master's Thesis"
 #let myUni = "Università degli studi di Padova"
 #let myDepartment = "Department of Mathematics ''Tullio Levi-Civita''"

preface/abstract.typ

@@ -13,8 +13,8 @@ In Computer Science, aliasing refers to the situation where two or more referenc
 On the one hand, aliasing can be useful in object-oriented programming, allowing programmers to implement designs involving sharing.
 On the other hand, aliasing poses significant challenges for formal verification since changing a reference can modify the data that other references also point to, making tracking values of references and predicting program behavior more difficult.
 
-Developed by JetBrains, Kotlin is an open-source, statically typed programming language that gained popularity in the recent years especially in the Android software development. However, unlike other programming languages, there are not many ad-hoc tools for performing formal verification in Kotlin. Moreover, Kotlin does not have a way to control aliasing, making formal verification a hard task for the language.
+Developed by JetBrains, Kotlin is an open-source, statically typed programming language that gained popularity in recent years especially in the Android software development field. However, unlike other programming languages, there are not many ad-hoc tools for performing formal verification in Kotlin. Moreover, Kotlin does not provide any guarantee on aliasing, making formal verification a hard task for the language.
 
-This work introduces an annotation system for Kotlin designed to control the uniqueness of references. After presenting and formalizing the annotation system, the thesis shows how to use these annotations for performing formal verification of Kotlin by encoding it into Viper, a language and suite of tools developed by ETH Zurich, providing an architecture for the development of new verification tools.
+This work introduces an annotation system for Kotlin designed to provide some guarantees on the uniqueness of references. After presenting and formalizing the annotation system, the thesis shows how to use these annotations for performing formal verification of Kotlin by encoding it into Viper, a language and suite of tools developed by ETH Zurich, providing an architecture for the development of new verification tools.
 
 #v(1fr)

preface/acknowledgements.typ

@@ -5,9 +5,18 @@
 #set page(numbering: "i")
 
 #align(right, [
-    #text(style: "italic", "Tieni l'infinito per ciò che lo merita...")
+    #box(align( 
+        start,
+        text(
+            style: "italic",
+            [“E il treno io l'ho preso e ho fatto bene \
+            Spago sulla mia valigia non ce n'era \
+            Solo un po' d'amore la teneva insieme \
+            Solo un po' di rancore la teneva insieme”]
+        )
+    ))
     #v(6pt)
-    #sym.dash#sym.dash#sym.dash T. V.
+    #sym.dash#sym.dash#sym.dash Francesco De Gregori
 ])
 
 #v(10em)