NuSMV is a new implementation and extension of SMV symbolic model checker, aimed for a reliable verification of industrially sized designs. The objective of this project is to model the Java Bytecode instruction flow of a program. With this model we can automatically check if a program respects the secure information flow property, which means certifying that there is no information leakage.
Every day about 20000 flights sail through the skies of the United States. Online a huge amount of data is available regarding each one of these flights, including information on delays, cancellations and their causes. From this data it’s possible to compute a large number of different statistics on mean delays, probability of cancellation, most probable delay cause etc. based on a single airport, route or airline. For this reasons we decided to create Skynet. Skynet is an application capable of gathering data from the U.S. Department of Transportation website through a web scraper implemented inside of it. The data is then analyzed, processed and distributed on multiple database realized through MongoDB and Neo4j technologies, which are necessary to achieve a good tradeoff between performances, reliability and availability.
A TFTP protocol is a simple lockstep File Transfer Protocol which allows a client to get a file from or put a file onto a remote host. This C implementation is suitable for embedded systems or for machines with limited resources.
The aim of this project was to build a secure online version of the famous table game Connect Four. We implemented the application using C language and the OpenSSL libraries. We also formally proved the protocols used during the communication between client and server with the BAN Logic formalism.
This project was made as part of the exam ‘Progettazione Web’ during my Bachelor’s degree. The main goals were to build a web application that would let users create or participate to events of various categories. The application is inspired from the famous EventBrite portal which is one of the most used in this sector.
Published in Journal 1, 2009
This paper is about the number 1. The number 2 is left for future work.
Recommended citation: Your Name, You. (2009). "Paper Title Number 1." Journal 1. 1(1). http://academicpages.github.io/files/paper1.pdf
Published in Journal 1, 2010
This paper is about the number 2. The number 3 is left for future work.
Recommended citation: Your Name, You. (2010). "Paper Title Number 2." Journal 1. 1(2). http://academicpages.github.io/files/paper2.pdf
Published in Journal 1, 2015
This paper is about the number 3. The number 4 is left for future work.
Recommended citation: Your Name, You. (2015). "Paper Title Number 3." Journal 1. 1(3). http://academicpages.github.io/files/paper3.pdf
Aggiornato:
This is a description of your talk, which is a markdown files that can be all markdown-ified like any other post. Yay markdown!
Aggiornato:
This is a description of your conference proceedings talk, note the different field in type. You can put anything in this field.
Undergraduate course, University 1, Department, 2014
This is a description of a teaching experience. You can use markdown like any other post.
Workshop, University 1, Department, 2015
This is a description of a teaching experience. You can use markdown like any other post.