Solar-Lezama Working on New NSF Project to Improve Computer Programming
13 April 2012
Assistant Professor Armando Solar-Lezama, a principal investigator at CSAIL, will join the University of Pennsylvania and seven other research institutions in a new National Science Foundation (NSF) project to make computer programming faster, easier and more intuitive. Dubbed ExCAPE (Expeditions in Computer Augmented Program Engineering), the project is a highly collaborative effort that will involve multiple research institutions, partners in industry, and educational outreach to the next generation of computer scientists.
The project was awarded a 5-year, $10 million grant as part of the NSF’s “Expeditions in Computing” program, which funds teams aiming ambitious, fundamental research agendas in computer science. The ExCAPE team includes researchers from the University of Pennsylvania, UC Berkeley, UCLA, Cornell, the University of Illinois at Urbana-Champaign, the University of Maryland, MIT, the University of Michigan, and Rice University.
“Computers have evolved at a dramatic pace, but the technology that's used to develop programs and software is evolving comparatively slowly,” said Rajeev Alur, the leader of the project and a professor of computer and information science in Penn’s School of Engineering and Applied Science. “What it means to ‘code’ hasn't changed much in the last 20-30 years. It's still done by expert programmers, and is quite time-consuming, expensive and error-prone.”
In today’s programming languages, programmers must write out explicit instructions for what they want the program to do. For large projects, this kind of coding is so complicated that programmers need separate “verification” teams to weed out errors.
Over the last two decades, this verification technology has matured, leading to powerful analysis tools that can find subtle mistakes in real-world systems. The ExCAPE approach will leverage these advances to help programmers avoid such mistakes in the first place.
The researchers are proposing an integrated toolkit for automated program synthesis. Such a toolkit would allow a programmer to essentially collaborate with a computer on writing a program, with each contributing the parts they are most suited to. With more powerful and integrated verification systems, the computer would be able to give feedback to the programmer about errors in the program, and even propose corrections.
"Let's say you want to program a robotic car for parallel parking," Alur said. "Instead of asking the programmer to write complete code in one particular style, we want to offer the programmer flexibility. The programmer can start by specifying high-level goals, such as the final desired car position and the requirement that there should be no collisions along the way.”
Automatically translating such goals directly to code is not yet feasible, so the programmer would still have to do some amount of coding to providing basic solution strategies for the program. For parallel parking, a strategy might correspond to a sequence of basic maneuvers: pull in front of the spot, back up straight, start turning, and finally, straighten out.
While this basic strategy for parallel parking is intuitive for humans, figuring out exactly when to start turning, and by how much, remains tricky. Humans, whether they are drivers or programmers, aren’t good at trying lots of combinations in search of the best one, but that’s exactly what computers are best suited to do.
Programming for robotic behavior is one of four real-word problem areas the ExCAPE team will test their research on. The researchers will work with programmers at AT&T, Coverity, Honeywell, IBM, Intel, Microsoft, and Willow Garage, to see if the synthesis tool is effective in meeting their coding challenges.
Other challenge areas involve figuring out how to set up routing policies for flow of information across networks of computers, how software written to work on single processor computers can be correctly translated to improve performance while running on multiple cores that are now common even in mobile devices, and how to design efficient and correct algorithms for coordinating decisions among multiple computers.
The researchers hope that this toolkit will change the public perception of computer science, and potentially, how it and other sciences are taught. The verification systems in the ExCAPE team’s synthesis toolkit could be applied to students working on high school algebra problems, for example, identifying flaws in logic that lead to incorrect answers. The toolkit’s smart feedback could even generate similar problems to test whether a student has learned from a mistake.
For more information on Solar-Lezama’s work, visit: http://people.csail.mit.edu/asolar/.