|
acm
The Association for Computing Machinery
|
| |
ACM HONORS CREATORS OF VERIFICATION TOOLS FOR SOFTWARE, HARDWARE
Team Developed Techniques Based on Analysis of Mathematical Models
|
| |
New York, NY, March 15, 2006 - The Association for Computing Machinery (ACM) has recognized four leading computer scientists for their contribution to techniques that provide powerful formal verification tools for hardware and software systems. Gerard J. Holzmann, Robert P. Kurshan, Moshe Y. Vardi, and Pierre Wolper demonstrated that checking the correctness of reactive systems can be achieved using a mathematical analysis of abstract machines. The four honorees will receive ACM's Paris Kanellakis Theory and Practice Award, which carries a $5,000 prize.
Holzmann is a researcher at NASA's Jet Propulsion Laboratory; Kurshan is a Fellow at Cadence Design Systems; Vardi is a Computer Science professor at Rice University; and Wolper is a Computer Science professor at Universite de Liege, Belgium.
The honorees addressed a key problem in computer science: finding ways to verify that hardware and software designs meet their specifications. This problem is particularly challenging in systems that interact with their environments, such as digital systems and communication protocols. These systems are characteristic of large telephone networks, and are known as reactive systems. Their techniques are widely used commercially in "control-intensive" computer programs.
The honorees demonstrated the use of mathematical analysis of formal models to check the correctness of these reactive systems. They showed how this approach yields algorithms which can be made efficient enough to make automated reasoning practical. Their body of work, in turn, provided the algorithmic foundations for the formal verification tools they were involved in developing.
About the Honorees
Gerard J. Holzmann earned his Ph.D. at Delft University of Technology, The Netherlands. A Fulbright Scholar, he worked at Bell Labs, a division of Lucent Technologies, from 1980 to 2003, and retired as director of computing principles research. He was awarded ACM's 2001 Software System Award for the design and development of a widely used software package called SPIN, which detects defects in networked computers, making them more reliable. Holzmann was elected to the National Academy of Engineering in 2005.
Before joining Cadence Design Systems, Robert P. Kurshan was a Distinguished Member of Technical Staff at Bell Laboratories. He received his Ph.D. in mathematics from the University of Washington, and spent two years as Visiting Professor at the Technion in Haifa, Israel. He has also taught courses at University of California Berkeley and New York University.
Moshe Y. Vardi is the George Professor in Computational Engineering and Director of the Computer and Information Technology Institute at Rice University. Prior to joining Rice in 1993, he managed the Mathematics and Related Computer Science Department at IBM Almaden Research Center. Vardi received his Ph.D. from the Hebrew University of Jerusalem. He is the author and co-author of nearly 300 technical papers as well as a book entitled "Reasoning about Knowledge." The recipient of three IBM Outstanding Innovations Awards, he is a co-winner of the 2000 Goedel Prize and a Fellow of ACM.
Pierre Wolper was a Member of Technical Staff at Bell Labs, then a division of AT&T, from 1982 to 1986. He received an undergraduate degree for the University of Liege, and a Ph.D. in Computer Science from Stanford University. The author of books and book chapters, he has published articles in many professional journals and conference proceedings. He shares the 2000 Goedel Prize with Moshe Vardi.
ACM will present the 2005 Kanellakis Award at its annual Awards Banquet on May 20, at the Westin St. Francis Hotel in San Francisco, CA.
The Paris Kanellakis Theory and Practice Award honors specific theoretical accomplishments that have had a significant and demonstrable effect on the practice of computing. This award is endowed by contributions from the Kanellakis family, with additional financial support provided by ACM's Special Interest Groups on Algorithms and Computational Theory (SIGACT), Special Interest Group on Design Automaton (SIGDA), Special Interest Group on Management of Data (SIGMOD), Special Interest Group on Programming Languages (SIGPLAN), the ACM SIG Project Fund, and individual contributions.
About ACM
ACM, the Association for Computing Machinery http://www.acm.org, is an educational and scientific society uniting the world's computing educators, researchers and professionals to inspire dialogue, share resources and address the field's challenges. ACM strengthens the profession's collective voice through strong leadership,
promotion of the highest standards, and recognition of technical excellence. ACM supports the professional growth of its members by providing opportunities for life-long learning, career development, and professional networking.
|
|
|
