From Philosophical to Industrial Logic

18^th March 2010, 15:00 Ashton Lecture Theatre
Professor Moshe Y. Vardi
Rice University

Abstract

One of the surprising developments in the area of program verification is how several ideas introduced by logicians in the first part of the 20th century ended up yielding at the start of the 21st century in industry-standard property-specification languages called PSL and SVA. This development was enabled by the equally unlikely transformation of the mathematical machinery of automata on infinite words, introduced in the early 1960s for second-order arithmetics, into effective algorithms for industrial model-checking tools. This talk attempts to trace the tangled threads of this development.

Biography

Moshe Y. Vardi is a Professor of Computer Science at Rice University, USA. His interests focus on applications of logic to computer science, including database theory, finite-model theory, knowledge in multi-agent systems, computer-aided verification and reasoning, and teaching logic across the curriculum. He is a renowned expert in model checking, constraint satisfaction and database theory, common knowledge (logic), and theoretical computer science.

Moshe Vardi chaired the Computer Science Department at Rice University from January 1994 until June 2002. Prior to joining Rice in 1993, he was at the IBM Almaden Research Center, where he managed the Mathematics and Related Computer Science Department. Dr Vardi received his Ph.D. from the Hebrew University of Jerusalem in 1981.

Vardi is the recipient of three IBM Outstanding Innovation Awards, a co-winner of the 2000 GKdel Prize, a co-winner of the 2005 ACM Paris Kanellakis Theory and Practice Award, and a co-winner of the LICS 2006 Test-of-Time Award. He holds honorary doctorates from Saarland University, Germany, and the University of Orleans, France. Dr Vardi is a Guggenheim Fellow, as well as a Fellow of the Association of Computing Machinery, the American Association for the Advancement of Science, and the American Association for Artificial Intelligence. He was designated Highly Cited Researcher by the Institute for Scientific Information, and was elected as a member of the US National Academy of Engineering, the European Academy of Sciences, and the Academia Europea. He has also co-chaired the ACM Task Force on Job Migration.