Problem: There are 40 two-sided tiles lying on a table, including 30 on their white side and 10 on their black side. With the lights off so that you can’t see the colors, divide the tiles into two piles with the same number of black tiles in each pile.
While many people would swear it can’t be done, computer scientists thrive on such puzzles.
“There’s usually a little grain of something in the puzzle, and if you get the trick you can solve it,” says CU-Boulder Assistant Professor Sriram Sankaranarayanan.
“It’s the kind of hunting we do,” he adds, alluding to the search for problems and their fixes in thousands of lines of code.
Sankaranarayanan is a specialist in cyber-physical systems, which are responsible for numerous control tasks in safety-critical systems such as automobiles, avionics, medical devices, and power distribution systems. From automobile braking systems to hospital ventilators and other life-saving devices, computer software is increasingly becoming the link between the operator and the physical system they seek to control.
Guaranteeing the correctness of these systems is naturally of the utmost importance. Sometimes a problem requires forensic, or afterthe- fact, analysis to determine why a particular system failed, but Sankaranarayanan prefers to work on program testing and verification at the front end of software development. “We want to be able to certify software in a car to be safe because the driver’s life depends on it,” he says.
He notes that NASA and the aerospace industry take verification of software systems very seriously due to the danger of flight and the millions of dollars that go into building aircraft and spacecraft. “Lots of people pore over the code, but they can’t automate verification fully.”
A lot of progress has been made over the last decade, and many common bugs can be found and fixed by automated program verification tools, he says. But there is still much more to do as software has become increasingly complex.
Sankaranarayanan compares it to following a race car with another race car. “We are always playing catch-up with what other people can do,” he says, explaining that viruses and computer hacking create additional threats to control systems.
“We want to bring an ethical hacking mentality to mathematics where we try to break systems in order to build them back up better.” Sankaranarayanan’s ultimate goal is to develop a software program that can verify another piece of software will do what it is supposed to do.
Although fully achieving that end may be inherently impossible, Sankaranarayanan says, he is making great enough strides for the National Science Foundation to award him its Faculty Early Career Development (CAREER) Award. The $460,000 grant will fund his innovative work on automatic analysis of cyber-physical systems for the next five years, with the goal of bridging the gap between research and industrial practice.
“I’m trying to push the boundary of what can be done today,” says the Stanford PhD graduate who went on to win the NEC Technology Commercialization Award at NEC Laboratories America in 2007. The award recognized his achievement in developing a framework for finding bugs in programs by combining abstract interpretation and model checking.
Sankaranarayanan has completed several other verification projects in the last few years, including one geared to drug infusion pumps in hospitals and another focusing on automotive control software.
Typically, he and his students try to integrate optimization tools and other techniques used by applied mathematicians in an ongoing attempt to isolate and develop innovative solutions.
“The lab is a real hotbed of activity,” he says, referring to about 15 faculty and students from both computer science and electrical and computer engineering who are working in related areas of study. “Our currency is in ideas.”
Other than the usual array of personal computers that would be expected for such an endeavor, several whiteboards, including one floorto- ceiling model, are installed around the group’s laboratory space. Equations scrawled as part of the day’s discourse at least partially cover these boards. One also posts a “riddle of the day.”
Sankaranarayanan speaks quietly with one student to offer a solution, and the student who posted the riddle nods appreciatively in reply.
Solution: Take 10 of the tiles aside and flip each one over to reveal the other color. Regardless of what color these tiles were originally, they now form a group with precisely the same number of black tiles as the remaining 30.
> Learn more at www.cs.colorado.edu/~srirams