Dino Distefano - Facebook Infer Static Analyser
Infer is an open-source static analyser developed at Facebook. Originally based on Separation Logic, Infer has lately evolved from a specific tool for heap-manipulating programs to a general framework which facilitates the implementation of new static analyses. In this talk, I will report on the Infer team’s experience of applying our tool to Facebook mobile code, each day helping thousands of engineers to build more reliable and secure software. Moreover, I will discuss the team’s current effort to turn Infer into a static analysis platform for research and development useful both to academic researchers and industrial practitioners.
Manuel Mazo Espinosa Jr. - Symbolic abstractions of control systems' timing behaviour
With the advent of the Internet-of-things and Cyber-Physical Systems everywhere, there has arisen a renewed interest on the study of networked control systems (NCS). NCS are systems in which measurements from sensors are sent through a communications network to a control unit to compute corrective actions for the system being monitored, actions which are again relayed through a network to actuators. In the past decade a shift of perspective in the design and analysis of NCS has emerged in order to make the use of communications bandwidth as efficient as possible. The idea is to move away from the traditional approach employing pre-determined (usually periodic) update times, to designs in which the time instants at which the control loop is closed is determined by the sensors themselves. This has resulted in what has been named “event-based control” (EBC). Despite of the many promising results of EBC designs I will argue that the unpredictability of the communications traffic they generate is a critical bottleneck to exploit EBC’s potential benefits. To solve this critical problem, I will describe our recent results on the construction of abstractions (in the form of timed automata) capturing the communications traffic of EBC. I will then describe how such abstractions can help in the design of more efficient EBC systems and schedulers for them.

© Università degli Studi di Roma "La Sapienza" - Piazzale Aldo Moro 5, 00185 Roma