A generic static analyzer and its application to TouchDevelop
Staff - Faculty of Informatics
Start date: 31 March 2015
End date: 1 April 2015
The Faculty of Informatics is pleased to announce a seminar given by Pietro Ferrara
DATE: Tuesday, March 31st 2015
PLACE: USI Lugano Campus, room A23, Red building (Via G. Buffi 13)
TIME: 10.30
ABSTRACT:
Sound static analysis aims at proving at compile time properties that are satisfied by all the runtime behaviors of a program. Generic modular static analyzers combine different approximations (for instance on numerical computations and heap structures), and apply them to prove properties on programs written in various programming languages.
In this talk, I will present Sample, a generic static analyzer based on the abstract interpretation theory, and its application to TouchDevelop programs.
Sample is language agnostic, and supports the modular automatic combination of expressive heap analyses (e.g., merging and splitting abstract heap nodes) with generic value domains. In the first part of the talk, I will present the overall design of Sample, and its main components.
In the second part of the talk, I will introduce the instantiation of Sample to TouchDevelop, a novel programming environment and language for developing mobile applications directly on mobile devices. We applied Sample into two distinct directions: (i) a safety analysis aimed at discovering possible bugs, and (ii) a cost analysis over approximating the number of iterations of loops. Despite the fact that the two analyses deal with quite different properties, they share the most part of the infrastructure, and in particular the implementation of the semantics of TouchDevelop and its APIs. The experimental results underline both the scalability and precision of the analysis, since Sample analyzes TouchDevelop programs in 5" on average, the 85% of the alarms are real bugs, and it infers bounds for the 70% of loops.
BIO:
Pietro has been a Research Staff Member in the group of Mobile Enterprise Software led by Marco Pistoia since July 2013. His main research interest is sound static analysis via abstract interpretation. In particular, he is currently working on various security (mostly confidentiality) properties of mobile (mostly Android) programs. Before joining IBM Research, Pietro was a lecturer at ETH of Zurich in the Programming methodology group under the supervision of Peter Mueller from April 2009 to July 2013. In this period, he developed Sample, a generic static analyzer developed in Scala that has been applied to a large variety of properties and programming languages. Previously, he was a PhD student from October 2005 to May 2009 at the Ecole Polytechnique of Paris and the Università Ca' Foscari of Venice on May, 22nd 2009 under the supervision of Radhia Cousot and Agostino Cortesi.
HOST: Prof. Mauro Pezzè
