On Hierarchical Communication Topologies in Message-passing Concurrent Systems
University of Oxford
COM1 Level 2
SR8, COM1-02-08
Abstract
In this talk, I will present recent work on automatic analysis of concurrent message-passing systems expressed in the pi-calculus, but motivated by ongoing work on an automatic safety verifier of Erlang programs, Soter. In the course of a computation, a concurrent system, such as an Erlang program, generates an unbounded set of processes (and of names), with a dynamically evolving communication topology. We are interested in the shape invariants satisfied by the communication topology, and the automatic inference of these invariants. We introduce the concept of "hierarchical" system, which is a pi-term whose communication topology is shaped by a finite forest T, specifying the hierarchical relationship between names. I will discuss the design of a static analysis to prove a term hierarchical by means of a novel type system that enjoys decidable inference. The soundness proof of the type system employs a non-standard view of pi-calculus reactions. The coverability problem for hierarchical terms is decidable, which is proved by showing that every hierarchical term is depth-bounded, an undecidable property known in the literature. We thus obtain an expressive static fragment of the pi-calculus with decidable safety verification problems. Time permitting, we will briefly discuss an application of such resource-bounded systems to the automatic verification of secrecy in the analysis of cryptographic protocols. (This is based on joint work with Emanuele D'Osualdo.)
[1] https://mjolnir.cs.ox.ac.uk/soter/
Biodata:
Luke Ong is Professor of Computer Science, University of Oxford; and Fellow of Merton College. He holds a BA in Mathematics (1984, Triple First) and a Postgraduate Diploma in Computer Science (1985, Distinction) from the University of Cambridge, and PhD in Computer Science (1988) from Imperial College London. Ong works in programming languages, verification and semantics and logic of computation. He is former General Chair of ACM/IEEE Symposium on Logic in Computer Science (LICS); Steering Committee Chair of Formal Structures in Computation and Deduction; and Vice Chair of ACM Special Interest Group in Logic and Computation (SIGLOG). He is a member of the Singapore Academic Research Council, and former chair of their Informatics and Mathematics Expert Panel; he is a judging panel member of the EACSL Ackermann Award and the EATCS Distinguished Dissertation Award. Ong has graduated 27 (and 8 current) doctoral students at Oxford. He is a joint winner of the 2017 ACM / EATCS Alonzo Church Prize for Outstanding Contributions in Logic and Computation.