From 9c4aa43e757437cbe6f5505234852d3bc591e1a4 Mon Sep 17 00:00:00 2001 From: francescoo22 Date: Tue, 2 Jul 2024 17:22:48 +0200 Subject: [PATCH] Update title --- chapters/5-Encoding.typ | 4 ++++ config/variables.typ | 2 +- preface/abstract.typ | 4 ++-- preface/acknowledgements.typ | 13 +++++++++++-- 4 files changed, 18 insertions(+), 5 deletions(-) diff --git a/chapters/5-Encoding.typ b/chapters/5-Encoding.typ index 05e0bba..add4678 100644 --- a/chapters/5-Encoding.typ +++ b/chapters/5-Encoding.typ @@ -1,2 +1,6 @@ #pagebreak(to:"odd") = Encoding in Viper +== Classes Encoding +== Functions Encoding +== Function Calls Encoding +== Predicates Unfolding diff --git a/config/variables.typ b/config/variables.typ index 53911a8..944f2d4 100644 --- a/config/variables.typ +++ b/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''" diff --git a/preface/abstract.typ b/preface/abstract.typ index 5943d6d..92baea2 100644 --- a/preface/abstract.typ +++ b/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) \ No newline at end of file diff --git a/preface/acknowledgements.typ b/preface/acknowledgements.typ index f58d05e..276294e 100644 --- a/preface/acknowledgements.typ +++ b/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)