• Moshe Vardi - Rice University (USA) (details)
• Yuxin Deng - East China Normal University (China) (details)
• Rob van Glabbeek - Data61, CSIRO (Australia); Stanford University (USA); University of New South Wales (Australia) (details)
• Bow-Yaw Wang - Academia Sinica (Taiwan) (details)

Prof. Moshe Vardi: The Siren Song of Temporal Synthesis

One of the most significant developments in the area of design verification over the last three decade is the development of algorithmic methods for verifying temporal specification of finite-state designs. A frequent criticism against this approach, however, is that verification is done after significant resources have already been invested in the development of the design. Since designs invariably contains errors, verification simply becomes part of the debugging process. The critics argue that the desired goal is to use temporal specification in the design development process in order to guarantee the development of correct designs. This is called temporal synthesis. In this talk I will review 60 years of research on the temporal synthesis problem, describe the automata-theoretic approach developed to solve this problem, and describe both successes and failures of this research program.

Moshe Y. Vardi is the George Distinguished Service Professor in Computational Engineering and Director of the Ken Kennedy Institute for Information Technology at Rice University. He is the recipient of three IBM Outstanding Innovation Awards, the ACM SIGACT Goedel Prize, the ACM Kanellakis Award, the ACM SIGMOD Codd Award, the Blaise Pascal Medal, the IEEE Computer Society Goode Award, the EATCS Distinguished Achievements Award, the Southeastern Universities Research Association's Distinguished Scientist Award, and the Church Award. He is the author and co-author of over 500 papers, as well as two books: "Reasoning about Knowledge" and "Finite Model Theory and Its Applications". He is a Fellow of the Association for Computing Machinery, the American Association for Artificial Intelligence, the American Association for the Advancement of Science, the European Association for Theoretical Computer Science, the Institute for Electrical and Electronic Engineers, and the Society for Industrial and Applied Mathematics. He is a member of the US National Academy of Engineering and National Academy of Science, the American Academy of Arts and Science, the European Academy of Science, and Academia Europaea. He holds honorary doctorates from the Saarland University in Germany, Orleans University in France, UFRGS in Brazil, and the University of Liege in Belgium. He is currently a Senior Editor of of the Communications of the ACM, after having served for a decade as Editor-in-Chief.

Prof. Yuxin Deng: Bisimulations for Probabilistic and Quantum Processes

Bisimulation is a fundamental concept in concurrency theory for comparing the behaviour of nondeterministic processes. It admits nice characterisations in many different ways such as fixed point theory, modal logics, game theory, coalgebras etc. In this talk, we review some key ideas used in the formulations and characterisations of reasonable notions of bisimulations for both probabilistic and quantum processes. To some extent the transition from probabilistic to quantum concurrency theory is smooth and natural. However, new ideas need also to be introduced. We have not yet reached the stage of formally verifying quantum communication protocols and quantum algorithms using bisimulations implemented by automatic tools. We discuss some recent efforts in this direction.

Yuxin Deng received his BEng (1999) and MSc (2002) from Shanghai Jiao Tong University, China, and PhD (2005) from Ecole des Mines de Paris, France. He was a research associate at University of New South Wales, Australia (2005-2006), an associate Professor at Shanghai Jiao Tong University, China (2006-2015), a visiting research fellow at Carnegie Mellon University, USA (2011), and a seconded expert at UNESCO Headquarters, France (2012-2014). In 2015 he joined East China Normal University as a full Professor. Dr. Deng’s research interests include concurrency theory, especially about process calculi, and formal semantics of programming languages, as well as formal verification of security protocols and distributed algorithms. He authored a book on the semantics of probabilistic processes.

Prof. Rob van Glabbeek: Is speed-independent mutual exclusion implementable?

A mutual exclusion algorithm is called speed independent if its correctness does not depend on the relative speed of the components. Famous mutual exclusion protocols such as Dekker's, Peterson's and Lamport's bakery are meant to be speed independent.
In this talk I argue that speed-independent mutual exclusion may not be implementable on standard hardware, depending on how we believe reading and writing to a memory location is really carried out. It can be implemented on electrical circuits, however.
This builds on previous work showing that mutual exclusion cannot be accurately modelled in standard process algebras.

Rob van Glabbeek has a strong international reputation in the study of the theory of concurrent computation, having made particular contributions to the conciliation of the interleaving and the true concurrency communities by codeveloping the current view of branching time and causality as orthogonal but interacting dimensions of concurrency. Some of his well known contributions are the linear time-branching time spectrum, branching bisimulation (with Peter Weijland), and action refinement (with Ursula Goltz). More recently, since 2015, he has worked with Peter Höfner on the notion of justness and on the (im)possibility of specifying fair schedulers or mutual exclusion protocols in standard process algebras. In addition, he has organised workshops on combining compositionality and concurrency, on logic, language and information, on the Unified Modelling Language, on workflow management, web services and business process modelling, on automatic and semi-automatic system verification, on structural operational semantics, and on formal methods for embedded systems. He is editor-in-chief of Electronic Proceedings in Theoretical Computer Science, a member of the editorial boards of Information and Computation and Theoretical Computer Science, and has been on several dozen program committees.

Prof. Bow-Yaw Wang: Verifying Assembly Codes for Practical Cryptography

Mathematical constructs are necessary for computation on the underlying algebraic structures of cryptosystems. They are often written in assembly languages and optimized manually for efficiency. We develop a hybrid technique to verify mathematical constructs implemented by assembly codes in OpenSSL and boringSSL. Our technique translates an algebraic specification of mathematical constructs into an algebraic problem. The algebraic problem in turn is solved by the computer algebra system Singular. The technique also translates overflow and range checking into the bit vector theory in SMT solvers. We report our case studies on verifying arithmetic computation over a large finite field in Curve25519 and NIST P-256, and the Montgomery Ladderstep in X25519.

Bow-Yaw Wang is a Research Fellow in Institute of Information Science, Academia Sinica, Taiwan. He was an Associate Research Fellow at Academia Sinica from 2008 to 2012, an INRIA Invited Professor from 2009 to 2011, an Invited Associate Professor at Tsinghua University from 2009 to 2010, an Adjoint Associate Professor at National Taiwan University from 2009 to 2012, an Assistant Research Fellow at Academia Sinica from 2003 to 2008, and an Adojoint Assistant Professor at National Taiwan University from 2004 to 2009. His research interest is logic and its application in computer science. He mainly works on formal verification. In the past, he has been working on compositional reasoning, program verification, learning-based verification techniques. More recently, he is interested in verifying assembly implementations of cryptographic primitives from security libraries such as OpenSSL and boringSSL. He is also running an interdisciplinary privacy research project at Academia Sinica.