Computer scientist Andrey Rybalchenko is one of the world's top 35 innovators under 35 years of age, according to MIT's Technology Review. The prestigious "TR35" list for 2010 is published in the September/October issue of the magazine. The honor goes to Rybalchenko, a professor at the Technische Universitaet Muenchen (TUM), for his work on software verification. From theoretical breakthroughs to practical development tools, the contributions of this 32-year-old have the potential to make the software that 21st-century civilization runs on more reliable.
When computer scientists agree that something is impossible, they mean it in a technically specific sense, like a rigorous mathematical proof. So when a promising new approach to a problem long considered impossible is proven theoretically - and then is demonstrated in a practical software program - that in itself marks not one but two major achievements. And when these insights and innovations address a problem with the potential to affect more or less everyone, every day, then the person responsible has done something truly extraordinary. This, in essence, describes the work for which Prof. Andrey Rybalchenko of the TUM Department of Informatics has been singled out.
The most familiar face of the problem Rybalchenko addressed, which people encounter as often at home as in the office, is an unresponsive program: Your computer is still running and the program hasn't crashed, but it has frozen up in the middle of some operation and gives you no clue why. Although the computer may still be able to perform other functions, it can't do what you want it to do. Every computer user is likely to have some choice words to describe the experience of staring at the rotating hourglass or colorful pinwheel displayed - endlessly - during this kind of failure, but the technical term is "liveness violation." A program fails to respond to a request from a user or from another program and enters a frozen condition, without even showing an error message. As annoying as such failures can be in personal computing, the consequences could be much more serious. Today the most basic elements of our infrastructure, from power and communications to air and rail transportation, from manufacturing to medicine, depend on the reliability of software systems. The same is true of safety, surveillance, and emergency response measures.
While tremendous progress has been made since the 1960s in automated software verification - that is, proving that certain kinds of failures are not lurking within millions of lines of computer code - liveness failures remained out of reach. In fact, since the 1930s "everyone knew" that a general solution to what computing pioneer Alan Turing termed the Halting Problem would be impossible. Andrey Rybalchenko resolved this theoretical impasse with the discovery of "transition invariants," a new principle for reasoning about liveness. In essence, he and collaborator Prof. Andreas Podelski (Albrecht-Ludwigs-Universitaet Freiburg) found a way to put liveness within the reach of a divide-and-conquer approach. Like other problems in computer science and software engineering, liveness reasoning could now be broken down into sub-tasks; so-called approximation techniques could now be applied to each sub-task; and the results could be combined to verify liveness properties for a software program.
Rybalchenko demonstrated the practical power of these insights by developing a verification tool called Terminator. Applied to the software for Windows device drivers, Terminator was able to show whether or not a driver's dispatch routines - the functions executed when the computer communicates with a printer or any other device - would always respond to the operating system when they were called. Through a collaboration with Byron Cook of Microsoft Research, Rybalchenko's innovative approach is now on a fast track from research demonstration to industrial software tool, giving him confidence, in his own words, "that liveness defects in mainstream software will eventually become extinct."
SOURCE
