The 19^th International Symposium on Automated Technology for Verification and Analysis

Sir Tony Hoare (C. A. R. Hoare) is a British computer scientist. He developed the sorting algorithm quicksort in 1959/1960. He also developed Hoare logic for verifying program correctness in 1969, and the formal language communicating sequential processes (CSP) to specify the interactions of concurrent processes in 1985. He received the Turing Prize and the Kyoto Prize for his fundamental contributions to the definition and design of programming languages in 1980 and 2000 respectively. Tony Hoare became a professor at Oxford University in 1977 where he is now an Emeritus Professor. Hoare was elected a Fellow of the Royal Society as well as a Fellow of the Royal Academy of Engineering. A recent personal research goal has been the unification of a diverse range of theories applying to different programming languages, paradigms, and implementation technologies. Tony has been and continue to be an inspiration to many researchers.

Title: A Geometric Theory for Program Testing

Abstract: Formal methods for verification of programs are extended to testing of programs. Their combination is intended lead to benefits in reliable program development, testing, and evolution. Our geometric theory of testing is intended to serve as the specification of a testing environment, included as the last stage of a toolchain that assists professional programmers, amateurs, and students of Computer Science. The testing environment includes an automated algorithm which locates errors in a test that has been run, and assists in correcting them. It does this by displaying, on a monitor screen, a stick diagram of causal chains in the execution of the program under test. The diagram can then be navigated backwards by in the familiar style of a satnav following roads a map.. This will reveal selections of places at which the program should be modified to remove the error.

Moshe Y. Vardi is University Professor, Karen Ostrum George Distinguished Service Professor in Computational Engineering at Rice University, where he is leading an Initiative on Technology, Culture, and Society. His interests focus on automated reasoning, a branch of Artificial Intelligence with broad applications to computer science, including machine learning, database theory, computational-complexity theory, knowledge in multi-agent systems, computer-aided verification, and teaching logic across the curriculum. He is also a Faculty Scholar at the Baker Institute for Public Policy at Rice University.

Title: Linear Temporal Logic: From Infinite to Finite Horizon

Abstract: Linear Temporal Logic (LTL), proposed in 1977 by Amir Pnueli for reasoning about ongoing programs, was defined over infinite traces. The motivation for this was the desire to model arbitrarily long computations. While this approach has been highly successful in the context of model checking, it has been less successful in the context of reactive synthesis, due to the chalenging algorithmics of infinite-horizon temporal synthesis. In this talk we show that focusing on finite-horizon temporal synthesis offers enough algorithmic advantages to compensate for the loss in expressiveness. In fact, finite-horizon reasonings is useful even in the context of infinite-horizon applications.

Professor Andrew Chi-Chih Yao is the Dean of Institute for Interdisciplinary Information Sciences (IIIS) in Tsinghua University. He is also the Distinguished Professor-at-Large in the Chinese University of Hong Kong. He was a full professor at Stanford University (1976 - 1981) and Princeton University (1986 - 2004). In 1996 he was awarded the Knuth Prize. He received the Turing Award, the most prestigious award in computer science, in 2000, "in recognition of his fundamental contributions to the theory of computation, including the complexity-based theory of pseudorandom number generation, cryptography, and communication complexity". In 2021 he received the Kyoto Prize in Advanced Technology.

Title: Probabilistic Reasoning in Machine Learning

Abstract: Traditionally, algorithms are designed with a particular problem in mind, supported by specific performance guarantees. The rise of powerful machine learning algorithms (ML) is a paradigm shift; yet determining what problems can be solved effectively by ML turns out to be a difficult task theoretically. In this talk, we present several new results in this direction. Notably, in some cases where ML is known to have poor performance in experiments, we give a rigorous proof using sophisticated probabilistic and geometric reasoning to confirm the observation. This important line of active research is still in its infancy, as seemingly intuitive conjectures are often hard to prove rigorously.

Prof. Somesh Jha received his B.Tech from Indian Institute of Technology, New Delhi in Electrical Engineering. He received his Ph.D. in Computer Science from Carnegie Mellon University under the supervision of Prof. Edmund Clarke (a Turing award winner). Currently, Somesh Jha is the Lubar Professor in the Computer Sciences Department at the University of Wisconsin (Madison). His work focuses on analysis of security protocols, survivability analysis, intrusion detection, formal methods for security, and analyzing malicious code. Recently, he has focussed his interested on privacy and adversarial ML (AML). Somesh Jha has published several articles in highly-refereed conferences and prominent journals. He has won numerous best-paper and distinguished-paper awards. Prof. Jha is the fellow of the ACM and IEEE.

Title: Trustworthy Machine Learning and the Security Mindset

Abstract: Fueled by massive amounts of data, models produced by machine-learning (ML) algorithms, especially deep neural networks (DNNs), are being used in diverse domains where trustworthiness is a concern, including automotive systems, finance, healthcare, natural language processing, and malware detection. Of particular concern is the use of ML algorithms in cyber-physical systems (CPS), such as self-driving cars and aviation, where an adversary can cause serious consequences. Interest in this area of research has simply exploded. In this work, we will emphasize the need for a security mindset in trustworthy machine learning, and then cover some lessons learned.