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.