Thesis.tex

% Setup and import
\documentclass[12pt,a4paper]{report}
\usepackage[english, italian]{babel}
\usepackage{csquotes}
\usepackage[dvipsnames]{xcolor}
\usepackage{newlfont}
\usepackage{algorithm}
\usepackage{algpseudocode}
\usepackage{amsmath}
\usepackage{biblatex}
\usepackage{forest}
\usepackage{hyperref}
\usepackage{multicol}
\usepackage{listings}
\usepackage{tikz}
\textwidth=450pt\oddsidemargin=0pt

% Dedication template
\newenvironment{dedication}
{
    \clearpage            % we want a new page
    \thispagestyle{empty} % no header and footer
    \vspace*{\stretch{1}} % some space at the top
    \itshape              % the text is in italics
    \raggedleft           % flush to the right margin
}
{
    \par                  % end the paragraph
    \vspace{\stretch{3}}  % space at bottom is three times that at the top
    \clearpage            % finish off the page
}

% Project Tree definition
\definecolor{folderbg}{RGB}{124,166,198}
\definecolor{folderborder}{RGB}{110,144,169}

\tikzset{
  folder/.pic={
    \filldraw[draw=folderborder,top color=folderbg!50,bottom color=folderbg]
      (-1.05*4pt,0.24pt+5pt) rectangle ++(.75*4pt,-0.24pt-5pt);  
    \filldraw[draw=folderborder,top color=folderbg!50,bottom color=folderbg]
      (-1.15*4pt,-4pt) rectangle (1.15*4pt,4pt);
  }
}

% Definition init
\newtheorem{definition}{Definition}[chapter]
\newtheorem{remark}{Remark}[definition]

% Setup algorithm numeration to follow the definition and remark ones
\renewcommand{\thealgorithm}{\arabic{chapter}.\arabic{algorithm}}

% Setup listings code style
\lstdefinestyle{mystyle}{
    backgroundcolor=\color{White},
    numberstyle=\tiny\color{Gray},
    commentstyle=\color{OliveGreen},
    keywordstyle=\color{MidnightBlue},
    stringstyle=\color{OrangeRed},
    basicstyle=\ttfamily\footnotesize,
    breakatwhitespace=false,
    breaklines=false,
    captionpos=b,
    keepspaces=true,
    numbers=left,
    numbersep=5pt,
    showspaces=false,
    showstringspaces=false,
    showtabs=false,
    tabsize=2
}
\lstset{style=mystyle}


% ForEach construct definition
\algnewcommand\algorithmicforeach{\textbf{for each}}
\algdef{S}[FOR]{ForEach}[1]{\algorithmicforeach\ #1\ \algorithmicdo}

% Tikz submodule import
\usetikzlibrary{automata, positioning, arrows}

\addbibresource{Bibliography.bib}

% Document start 
\begin{document}


% Title page
\begin{titlepage}
    \begin{center}
        {{\Large{\textsc{Alma Mater Studiorum $\cdot$ Universit\`a di
                            Bologna}}}} \rule[0.1cm]{15.8cm}{0.1mm}
        \rule[0.5cm]{15.8cm}{0.6mm}
        {\small{\bf SCUOLA DI SCIENZE\\
                Corso di Laurea in Informatica }}
    \end{center}
    \vspace{15mm}
    \begin{center}
        {\LARGE{\bf Choreia: A Static Analyzer }}\\
        \vspace{3mm}
        {\LARGE{\bf to Generate Choreography Automata}}\\
        \vspace{3mm}
        {\LARGE{\bf from Go Source Code}}\\
    \end{center}
    \vspace{40mm}
    \par
    \noindent
    \begin{minipage}[t]{0.47\textwidth}
        {\large{\bf Relatore:\\
                Prof. Ivan Lanese}}
    \end{minipage}
    \hfill
    \begin{minipage}[t]{0.47\textwidth}\raggedleft
        {\large{\bf Presentata da:\\
                Enea Guidi}}
    \end{minipage}
    \vspace{20mm}
    \begin{center}
        {\large{\bf Sessione III\\
                Anno Accademico 2020/2021 }}
    \end{center}
\end{titlepage}


% Dedication page
\begin{dedication}
    Alla mia famiglia e agli amici che\\
    mi hanno accompagnato in questo viaggio
\end{dedication}


% Abstract
\begin{abstract}
    Le coreografie sono un paradigma emergente per la descrizione dei sistemi concorrenti che sta prendendo piede negli ultimi anni. Lo scopo principale è quello di fornire al programmatore uno strumento che permetta di capire in maniera immediata il \emph{comportamento} dei partecipanti all'interno del sistema e come questi interagiscono tra loro. Partendo dai singoli partecipanti, e le loro \emph{viste locali}, è possibile ricomporre in maniera bottom-up l'intera coreografia (o \emph{vista globale}) del sistema.
    Un ulteriore vantaggio delle coreografie è che, quando rispettano alcune proprietà definite, danno garanzie sull'assenza di tipici problemi di concorrenza quali Deadlocks, Liveness e Race Conditions.
    Esistono vari modelli formali di coreografie, questa tesi tratta nello specifico i \emph{Choreography Automata}, basati su \emph{Finite State Automata} (FSA).
    In questa tesi viene presentato Choreia: un tool di analisi statica che, partendo da un codice sorgente Go, ricava il Choreography Automaton del sistema concorrente in maniera bottom-up.
\end{abstract}

% Auto-generated table of contents
\tableofcontents

% "Introduction" chapter
\input{Chapters/Introduction.tex}

% "Preliminaries and Notation" chapter
\input{Chapters/Preliminaries.tex}

% "Technology stack" chapter
\input{Chapters/Technologies.tex}

% "Changes and adaptations" chapter
\input{Chapters/Adaptations.tex}

% "Tool description" chapter
\input{Chapters/Tool.tex}

% "Conclusion and future works" chapter
\input{Chapters/Conclusions.tex}

\printbibliography

\end{document}