Automated Reasoning Creates More Reliable Computing Systems

Algorithmic verification techniques provide foundations for software and hardware reliability

Much of civilization now relies upon the foundations of software and hardware. Whether we are aware of software and hardware’s impact, for many of us, it overwhelms most of our daily tasks, including our working hours with computers and cell phones but also the technologies that keeps our cars running and our planes flying. Dr. Moshe Vardi, of Rice University, helps develop techniques that can be used by industry to work towards creating more reliable systems. Using algorithmic verification techniques, Dr. Vardi enables computers to analyze computer programs and ensure that they meet their desired functionality, which makes his research highly important to society. Therefore, it is through the continual improvements of more reliable systems that Dr. Vardi and his team do the behind-the-scenes research that is necessary for life as we know it and for continued development towards more sophisticated technologies and applications.

Central to Dr. Vardi’s work is a focus upon automated reasoning, which is the ability of computers to reason symbolically. The symbolic language is the language of logic, which has been studied by philosophers for 2,500 years. In the past fifty years, this language has found numerous applications in computer science. Dr. Vardi is capitalizing upon these applications to produce reliable systems that integrate the knowledge of designers and the needs of the consumer. This process allows for the interaction between designer and consumer to communicate in a more intuitive way and leads to product development that is both faster and cheaper, while being more in sync with the expectations of the consumer. Dr. Vardi’s work with his students at Rice, as well as with collaborators all over the world, including Chile, China, India, Israel,and Italy, helps to make the interface between people and computer systems more reliable and valuable for our society at a whole.

Current research includes:

  • Formal Requirements: Dr. Vardi works to create programs that have formal requirements that work well and are designed to perform what a consumer needs them to do. Much of his research aims at understanding what works well with formal requirements in addition to being sure that they are compliant.

  • How can the Computer do more Work? Once formal requirements have been written, Dr. Vardi is hoping to make the computer do more of the work for designers. He and his team hope to design a system that will allow a designer to write the requirements and then have the computer convert the requirements into a more refined design for the program.

Bio

Moshe Y. Vardi is Karen Ostrum George Distinguished Service Professor in Computational Engineering and Director of the Ken Kennedy Institute for Information Technology at Rice University. His interests focus on automated reasoning, a branch of Artificial Intelligence with broad applications to computer science, including database theory, computational-complexity theory, knowledge in multi-agent systems, computer-aided design and verification, and teaching logic across the curriculum.

Dr. Vardi has been fascinated by science since his youth. He discovered computer programming at age sixteen, when he saw an advertisement in the newspaper for computer programming. Growing up in Israel in the 1960’s, Dr. Vardi had little experience with computers, let alone being around them. His curiosity led him to ask his father for money to go to a two-week programming school. His father’s agreement led Dr. Vardi to a lifetime of passion for programming. Now, as a computer scientist, he is excited to continue to push the frontier of knowledge.

In his free time, aside from research, Dr. Vardi does not stray far from his passion for computer science and technology; even out of the office, Dr. Vardi is working with social scientists to understand the societal consequences of information technology.

Website: www.cs.rice.edu/~vardi

In the News

Publications

An automata-theoretic approach to automatic program verification

PDF

Memory-efficient algorithms for the verification of temporal properties

PDF

Model checking of safety properties

PDF

The ForSpec temporal logic: A new temporal property-specification language

PDF

A scalable and nearly uniform generator of SAT witnesses

PDF

Awards

April 2013 Southeastern Universities Research Association's Distinguished Scientist Award

May 2011 IEEE Computer Society's 2011 Harry H. Goode Memorial Award

November 2008 Blaise Pascal Medal, European Academy of Sciences

May 2006 ACM Paris Kanellakis Award for Theory and Practice

February 2002 Member, U.S. National Academy of Engineering

Patents

Directly verifying a black-box system, US Patent 6,526,544, Feb. 25, 2003.

System and method to analyze VLSI designs, US Patent 7,203,621, April 10, 2007.