Javier Esparza, TU Munich
Javier Esparza holds the Chair for Foundations of Software Reliability and Theoretical Computer Science at the Technische Universität München since 2007. Previously he held the Chair of Software Reliability and Security at the University of Stuttgart (2003-2007), the Chair of Theoretical Computer Science at the University of Edinburgh (2001-2003), and worked as Associate Professor at the Technische Universität München (1994-2001). He has co-authored a book on Free Choice Petri nets with Jörg Desel, and a book on the unfolding approach to Model Checking with Keijo Heljanko. He has published over 150 scientific papers in the fields of automatic program verification, program analysis, concurrency theory, and automata theory. Javier Esparza has contributed to the theory Petri nets, and was one of the initiators of the unfolding approach to model checking, the automata-theoretic approach to software model checking, and the verification of infinite-state systems. More recently he has conducted research on the fundamentals of program analysis and the verification of parametrized and stochastic systems. His group has developed several verification tools, including Moped and jMoped and Rabinizer. Javier Esparza received a honorary doctorate in Informatics from the Masaryk University of Brno in 2009, is member of Academia Europaea since 2011, and received an ERC Advanced Grant in 2018.
Population protocols: A Case Study in Parameterized Verification of Liveness Properties of Probabilistic Distributed Algorithms
Many distributed algorithms should be correct independently of the number of processes executing them. Examples include algorithms for mutual exclusion, leader election, distributed termination, distributed consensus, reliable broadcast, etc. We say that these systems are parametric in the number of processes, and call them parameterized systems.
When the number of processes is fixed, many parameterized systems have a finite state space, and their correctness can be automatically analyzed using e.g. model-checking techniques. The challenge of parameterized verification is to automatically prove correctness for any number of processes. It amounts to proving that each member of an infinite family of finite-state systems is correct.
Population protocols are a model of computation very much studied by the distributed systems community. They are used to describe and analyze algorithms able to run in arbitrary networks of unknown topology. The goal of a protocol is that all processes learn some information about the initial configuration of the network. More precisely, in a protocol with initial states q_1, …, q_n, all processes should learn whether P(x_1, …, x_n) holds, where P is a given predicate, and x_i denotes the initial number of agents in q_i.
Population protocols are a great testbed for parameterized verification techniques. In the talk I will introduce them, discuss their expressive power, and analyze the theory and practice of proving them correct.
Mauro Pezzè, Università della Svizzera italiana and Università degli studi di Milano Bicocca
Mauro Pezzè is a professor of software engineering at USI – Università della Svizzera Italiana, Lugano, Switzerland, where he coordinates the STAR – Software Testing and Analysis research Lab, and where he served as Dean. Mauro Pezzè is also a professor at the Università degli studi di Milano Bicocca, where he coordinates the LTA – Laboratory for Software Testing and Analysis. Mauro Pezzè is editor in chief of ACM TOSEM Transactions on Software Engineering and Methodology, and served in the editorial board of IEEE TSE Transactions on Software Engineering and STVR, the International Journal of Software Testing, Analysis and Verification. He served as program chair of ICSE, the International Conference on Software Engineering, in 2012, and program and general chair of ISSTA, the ACM International Symposium on Software Testing and Analysis, in 2006 and 2013, respectively. He is the co-author of an influential book ‘Software Testing and Analysis, Process, Principle and Techniques,’ and is known for his work on software testing, program analysis, self-healing and self-adaptive software systems.
During his career, Mauro Pezzè had the opportunity to visit as student, research and professor the University of Edinburg, the University of California Irvine and the National University of Singapore, and has advised over 35 PhD students, many of which are prominent members of the academic and industrial communities.
Automatic Verification of Human-Centric Cyber-Physical Systems
Human-centric cyber-physical systems (HCPhS) are systems where software, devices, machine learning and people seamlessly and endlessly interact with evolving goals, requirements and constraints. They are increasingly pervading our life, and span from simple mobile and Web applications, like recommendation systems and virtual shops, to complex evolving systems, like autonomous vehicles and smart cities. In this talk, I will give a broad and visionary view of the emerging issues and opportunities in the verification of human-centric cyber-physical systems. I will introduce the main features and survey the main open challenges of verifying human-centric cyber-physical systems. I will discuss scope and limitation of the most recent research results in software verification with particular focus on software testing; I will overview the ongoing partial but promising research activities in our USI-Star and UniMiB-LTA laboratories, and I will propose my vision of the most challenging open research issues.
Nikos Gorogiannis, Facebook
Nikos works with the Facebook Infer team on static analysis, and as a Senior Lecturer in Computer Science at Middlesex University. He is interested in applied verification, logic and automated reasoning. He previously led the development of Cyclist, a theorem prover based on cyclic proof, and worked on several decision procedures and complexity results for separation logic.
Concurrency bug detection at scale with Infer
Concurrency bugs are notoriously difficult to reason about in program verification. I will present two static analyses deployed at Facebook for detecting (a) data races and (b) deadlocks, both for Java code. These analyses have low-FP rates as a core design goal, and are implemented in the open-source Infer analyser. I will discuss the design trade-offs of these analyses, our experience from deploying them in production, as well as related theoretical results.