Title: DyNetKAT: An Algebra of Dynamic Networks

Abstract. In this talk I will introduce DyNetKAT -a formal language for specifying dynamic updates for Software Defined Networks. The latter can play an important role in solving issues concerning big data applications, including data processing in cloud data centers, optimisations and data delivery. DyNetKAT builds upon Network Kleene Algebra with Tests (NetKAT) and adds constructs for synchronisations and multi-packet behaviour to capture the interaction between the control- and data plane in dynamic updates. A sound and ground-complete axiomatisation of DyNetKAT will be discussed, together with an efficient method for reasoning about safety properties, and associated case studies.

Title: Causal Reasoning in Systems

Abstract. Causal inference plays an important role in assessing why did a hazardous situation occur and how certain undesired scenarios could have been avoided, or when performing fault localisation in systems, amongst others. In this talk I will introduce a notion of “actual causality”, proposed by Joseph Halpern and Judea Pearl in their seminal work “Causes and explanations: A structural-model approach”. An adoption to the setting of transition systems and, implicitly, DyNetKAT models, will be discussed as well. As we shall see, causal inference for DyNetKAT enables addressing interesting questions such as Reachability: “Can host A communicate with host B? Can every host communicate with every other host?”, or Security: “Does all untrusted traffic pass through the intrusion detection system located at C?”.