Parallel and distributed programming is notoriously hard. Many languages and software toolkits address the challenge by offering high-level abstractions, built on actors, domain specific languages or informal English descriptions; they allow for intuitive reasoning, but do not formally ensure that a set of decentralised components follow a given specification.

To address this problem, the talk will present how we can use a specification based on Multiparty Session Types (MPST) to explore hybrid dynamic verification of parallel programming and distributed tracing.

The talk first quickly introduces MPST and then demonstrates its usability with applications for

(1) refinement dynamic checking for Rust and TypeScript languages; and (2) a distributed tracing tool (OpenTelemetry) for Cloud Computing.

The talk concludes some open questions on specification-guided runtime verification.

Nobuko Yoshida is Professor of Computing at Imperial College London. She is currently an EPSRC Established Career Fellow at Imperial College London and Honorary Senior Research Fellowship of University of Glasgow. In November 2020, she was awarded a Suffrage Science Award for her work on EDI.

Last 10 years, her main research interests are theories and applications of protocols specifications and verifications. She introduced multiparty session types [POPL’08,JACM] which received Most Influential POPL Paper Award in 2018 (judged by its influence over the last decade). This work enlarged the community and widened the scope of applications of session types, e.g. runtime monitoring based on Scribble (co-developed with Red Hat) has been deployed to other projects such as cyberinfrastructure in the US Ocean Observatories Initiative (OOI); and widened the scope of her research areas.

She is an editorial board member of ACM Transactions on Programming Languages and Systems, ACM Formal Aspects of Computing, Acta Infomatica, Journal of Logical Algebraic Methods in Programming, Mathematical Structures in Computer Science, and the chief editor of The Computer-aided Verification and Concurrency Column for EATCS Bulletin.

Her current industry partners include: Actyx AG, Barclays, Cognizant, Codeplay Software Ltd, Coveo Solutions Inc., Estafet, Google, J.P. Morgan, Microsoft, Red Hat, Weaveworks, Erlang Solutions Ltd, Quviq AB, TATA Consultancy Services, ABB, Arm, EDF Energy, Xilinx, EPCC Ltd and UltraSoC Technologies Ltd.