[pl-seminar] Special madPL seminar on Thursday at 2

["Loris D'Antoni" <loris@xxxxxxxxxxx>]

This Thursday we will have a special madPL seminar at 2 pm in CS4310

Speaker: Adrian Francalanza

Title: Consistently-Detecting Monitors

Abstract:

Monitors are computational entities that observe the executions of other entities (systems) with the aim of accruing system information, comparing system executions against some behavioural specification, or reacting to the observed system executions via adaptation or enforcement procedures. Monitors are typically considered to be part of the Trusted Computing Base and, consequently, their descriptions are expected to be correct. A correctness requirement often presumed of monitors is that they should exhibit deterministic behaviour. Yet, for most monitoring frameworks, such a requirement is seldom specified in unambiguous terms or shown to hold.

In this talk I present a study of a contextual definition for deterministic monitoring based on the observed behaviour of a monitor (i.e., detections) when it is instrumented over arbitrary systems. I give an alternative, coinductive definition based on the notion of controllability which does not rely on system quantifications, and show that it is fully-abstract with respect to the former definition. I then present the development of a symbolic counterpart to the controllability definition that facilitates an automated analysis for controllable monitors involving data.


Bio:

Adrian Francalanza obtained his PhD from Sussex University, working on co-inductive theories for partial-failure and fault tolerance in a distributed pi-calculus. During his post-doctorate, he worked on ownership types for object-oriented languages at Imperial College, and then on separation-based logics for message-passing languages at Southampton University. Since arriving at the University of Malta, he worked on various aspects related to runtime verification. He has studied the monitorability of various system specifications, investigated compositional theories for monitors, and developed analysis tools for languages such as Erlang, Java and C. He also worked on developing substructural type systems for concurrent programs with explicit memory allocation and deallocation, and studied typed behavioural theories induced by these type systems.