Campus Event Calendar
Event Entry
What and Who
From Lowenheim to PSL
Moshe Vardi
Rice University
SWS Distinguished Lecture Series
Moshe Y. Vardi is the George Professor in Computational Engineering and Director of the Computer and Information Technology Institute at Rice University. He chaired the Computer Science Department at Rice University from January 1994 till 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. His research interests include database systems, computational-complexity theory, multi-agent systems, and design specification and verification. Vardi received his Ph.D. from the Hebrew University of Jerusalem in 1981. He is the author and co-author of over 300 technical papers, as well as two books, "Reasoning about Knowledge" and "Finite Model Theory and Its Applications", and the editor of several collections.
Vardi is the recipient of three IBM Outstanding Innovation Awards, a co-winner of the 2000 Goedel Prize, a co-winner of the 2005 ACM Paris Kanellakis Award for Theory and Practice, and a co-winner of the LICS 2006 Test-of-Time Award. He holds honorary doctorates from the University of Saarland, Germany, and the University of Orleans, France. Vardi is an editor of several international journals and the president of the International Federation of Computational Logicians. He is 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 recently co-chaired the ACM Task Force on Job Migration
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, RG2
Expert Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Wednesday, 12 December 2007
17:00
60 Minutes
G26
building 42, lecture hall 110
Kaiserslautern
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 an
industrial-standard property-specification language called PSL. 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 model-checking tools. This talk attempts to trace the tangled threads
of this development.
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 an
industrial-standard property-specification language called PSL. 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 model-checking tools. This talk attempts to trace the tangled threads
of this development.
Contact
Brigitta Hansen
0681 - 9325200
--email hidden
passcode not visible
logged in users only
Brigitta Hansen, 11/26/2007 14:32
Brigitta Hansen, 11/26/2007 14:31 -- Created document.
Brigitta Hansen, 11/26/2007 14:31 -- Created document.