Automated System Verification (2016/2017)

Course code
Name of lecturer
Nicola Fausto Spoto
Nicola Fausto Spoto
Number of ECTS credits allocated
Academic sector
Language of instruction
II sem. dal Mar 1, 2017 al Jun 9, 2017.

Lesson timetable

II sem.
Day Time Type Place Note
Monday 8:30 AM - 11:30 AM lesson Lecture Hall I  
Tuesday 2:30 PM - 4:30 PM laboratorio Laboratory Laboratorio Ciberfisico from Mar 14, 2017  to Jun 9, 2017
Tuesday 4:30 PM - 6:30 PM lesson Lecture Hall I  

Learning outcomes

The goal of this course is to present techniques for programming and verifying concurrent software systems, also applied to mobile computing. It presents the syntactical constructs, their semantics and the techniques for concurrent programming, the problems induced by concurrency and the possibility of verification through automatic tools. It presents the development of concurrent web services through servlets. Hence it describes techniques for mobile software development, typically consuming web services, where concurrency is more and more extensively used. The course uses the Java programming language and the Android framework as concrete contexts for development.


Concurrent programming, motivations and problems
Java memory model
Constructs and libraries for concurrency in Java
Verification of concurrent systems: code annotation and static analysis
Programming web services through Java servlets
Mobile programming and its specific problems
Mobile interfaces and their usability
Design patterns for mobile interfaces
Android components and intents
Android user interfaces
Android concurrency
The MVC pattern applied to Android
The master/detail pattern in Android
Querying web services from Android

Reference books
Author Title Publisher Year ISBN Note
G. Blake Meike Android Concurrency (Edizione 1) Addison-Wesley 2016 978-0-13-417743-4 Testo di supporto per approfondimento, non essenziale
Bill Phillips et al. Android Programming - The Big Nerd Ranch Guide (Edizione 2) Big Nerd Ranch 2015 978-0134171456 Testo di supporto per approfondimento, non essenziale
Brian Goetz et al Java Concurrency in Practice (Edizione 1) Addison-Wesley 2015 978-0-321-34960-6 Testo didattico consigliato, essenziale per seguire il corso

Assessment methods and criteria

Development of a concurrent application in Android. Presentation and oral dissertation about the code of the application.

Teaching aids